proposition: Lemma compose_axioms : forall a b c f g : E, axioms b c f -> axioms a b g -> axioms a c (Function.compose f g).
proof: Proof. ir. unfold axioms in H, H0; xd. assert (Function.composable f g). unfold Function.composable in |- *. xd. rewrite H3; am. unfold axioms in |- *; xd. ap Function.compose_axioms. rewrite Function.composable_domain; au. unfold sub in |- *; ir. assert (Function.axioms (Function.compose f g)). ap Function.compose_axioms. pose (Function.range_ex H7 H6). nin e; xd. pose (Function.compose_ev H8). rewrite H9 in e. rewrite e. ap H4. ap Function.range_inc. am. apply ex_intro with (V x0 g); xd. unfold Function.composable in H5; xd. ap H11. ap Function.range_inc. am. apply ex_intro with x0; xd. assert (Function.domain (Function.compose f g) = Function.domain g). ap Function.composable_domain. unfold Function.composable in |- *; xd. rewrite <- H12. am. Qed.
imports: set_theory