proposition: Lemma function_extensionality : forall f g : E, axioms f -> axioms g -> (forall x : E, defined f x -> defined g x) -> (forall x : E, defined g x -> defined f x) -> (forall x : E, defined f x -> V x f = V x g) -> f = g.
proof: Proof. ir. ap extensionality. ap function_sub; au. ap function_sub; au. ir. sy. ap H3. ap H2. am. Qed.
imports: set_theory