Axiom (Axiom of Extensionality) VA VBVx:(x∈A→x∈B)→A=B. Theorem(The Principle of Functional Extensionality) f,g are functions: f=g→dom(f)=dom(g)∧（付x∈dom(f):f(x)=g(x)） fg(a,b):(a,b)∈f→(a,b)∈g)→f=g It may be that cod(f)cod(g). Hengfeng Wei (hfweixinju.edu.cn) 1-10 Set Theory (III):Functions 2019年12月10日13/40Axiom (Axiom of Extensionality) ∀A ∀B ∀x : (x ∈ A ⇐⇒ x ∈ B) ⇐⇒ A = B. Theorem (The Principle of Functional Extensionality) f, g are functions : f = g ⇐⇒ dom(f) = dom(g) ∧ ( ∀x ∈ dom(f) : f(x) = g(x) ) ∀f ∀g ∀(a, b) : ((a, b) ∈ f ⇐⇒ (a, b) ∈ g) ⇐⇒ f = g. It may be that cod(f) ̸= cod(g). Hengfeng Wei (hfwei@nju.edu.cn) 1-10 Set Theory (III): Functions 2019 年 12 月 10 日 13 / 40