proposition: Lemma UA_iso_law1 : AreIsos UA_iso_mor UA_iso_mor_1.
proof: Proof. unfold AreIsos in |- *; split; unfold RIso_law in |- *. apply Trans with (UA_diese u2 (UA_mor u2)). apply UA_unic. apply Trans with (UA_mor u2 o FMor G (UA_diese u2 (UA_mor u1)) o FMor G (UA_diese u1 (UA_mor u2))). apply Comp_l; apply FComp. apply Trans with ((UA_mor u2 o FMor G (UA_diese u2 (UA_mor u1))) o FMor G (UA_diese u1 (UA_mor u2))). apply Ass. apply Trans with (UA_mor u1 o FMor G (UA_diese u1 (UA_mor u2))). apply Comp_r; apply UA_diag. apply UA_diag. apply UA_unic1. apply Trans with (UA_mor u2 o Id (G (UA_ob u2))). apply Comp_l; apply FId. apply Idr1. apply Trans with (UA_diese u1 (UA_mor u1)). apply UA_unic. apply Trans with (UA_mor u1 o FMor G (UA_diese u1 (UA_mor u2)) o FMor G (UA_diese u2 (UA_mor u1))). apply Comp_l; apply FComp. apply Trans with ((UA_mor u1 o FMor G (UA_diese u1 (UA_mor u2))) o FMor G (UA_diese u2 (UA_mor u1))). apply Ass. apply Trans with (UA_mor u2 o FMor G (UA_diese u2 (UA_mor u1))). apply Comp_r; apply UA_diag. apply UA_diag. apply UA_unic1. apply Trans with (UA_mor u1 o Id (G (UA_ob u1))). apply Comp_l; apply FId. apply Idr1. Qed.
imports: CatProperty Functor