proposition: Lemma function_sub : forall f g : E, axioms f -> axioms g -> (forall x : E, defined f x -> defined g x) -> (forall x : E, defined f x -> V x f = V x g) -> sub f g.
proof: Proof. ir. unfold sub in |- *. ir. set (K := lem1 H H3) in *. assert (defined f (pr1 x)). unfold defined in |- *; xd. unfold domain in |- *. ap Image.incl. am. assert (V (pr1 x) f = V (pr1 x) g). ap H2. am. rewrite K. assert (defined g (pr1 x)). ap H1. am. unfold defined in H6. xd. unfold domain in H7. set (K1 := Image.ex H7) in *. nin K1. nin H8. unfold axioms in H0. set (K1 := lem1 H6 H8) in *. rewrite H9 in K1. rewrite H5. rewrite <- K1. am. Qed.
imports: set_theory