proposition: Lemma Comp_com_law : Com_law Comp_com_mor.
proof: Proof. unfold Com_law, Comp_com_mor in |- *. apply Trans with (Mor_com_ob bxg o FMor G (Mor_com_arrow g)). apply (Prf_com_law g). apply Trans with (Mor_com_ob axf o FMor G (Mor_com_arrow f) o FMor G (Mor_com_arrow g)). apply Trans with ((Mor_com_ob axf o FMor G (Mor_com_arrow f)) o FMor G (Mor_com_arrow g)). apply Comp_r; apply (Prf_com_law f). apply Ass1. apply Comp_l; apply FComp1. Qed.
imports: Functor