proposition: Lemma Epic_Equalizer_iso : forall p : Epic_law (E_mor f), let f1 := E_diese f (Epic_Equalizer_id p) in AreIsos (E_mor f) f1.
proof: Proof. intros p. unfold AreIsos, RIso_law in |- *; split. apply Sym; apply (Prf_E_law2 f (Epic_Equalizer_id p)). apply E_monic. apply Trans with (E_mor f o Id a). apply Trans with (E_mor f o E_diese f (Epic_Equalizer_id p) o E_mor f). apply Ass1. apply Comp_l. apply Sym; apply (Prf_E_law2 f (Epic_Equalizer_id p)). apply Trans with (E_mor f). apply Idr1. apply Idl1. Qed.
imports: CatProperty