proposition: Lemma fcompose_axioms : forall f g, axioms f -> axioms g -> source f = target g -> axioms (fcompose f g).
proof: Proof. ir. uf fcompose. change (axioms (create (source g) (target f) (fun y => fmor f (fmor g y)))). ap create_axioms. sh (fun x => fob f (fob g x)). uhg; dj. uh H0; ee; am. uh H; ee; am. ap ob_fob. am. rw H1. ap ob_fob. am. am. rw id_fob. ap uneq. rw H1. ap id_fob. am. am. am. rw H1; ap ob_fob; am. ap mor_fmor. am. rw H1. ap mor_fmor. am. am. rw source_fmor. ap uneq. rw source_fmor. tv. am. am. am. rw H1; ap mor_fmor; am. rw target_fmor. ap uneq. rw target_fmor. tv. am. am. am. rw H1; ap mor_fmor; am. rw comp_fmor. ap uneq. rw H1. ap comp_fmor. am. am. am. am. am. rw H1. fw. rw H1. fw. fw. rww H11. Qed.
imports: Arith category