proposition: Lemma Eq_fg : f =_S g.
proof: Proof. generalize (Equalizer_iso (f:=Thi2_D_E_fg) Thi2_e1_RightInv). intro H; elim H. intros H2 H3. apply Trans with ((E_diese Thi2_D_E_fg (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv) o Thi2_e1) o f). apply Trans with (Id Thi2_v o f). apply Idl1. apply Comp_r. apply Sym; apply H2. apply Trans with ((E_diese Thi2_D_E_fg (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv) o Thi2_e1) o g). apply Trans with (E_diese Thi2_D_E_fg (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv) o Thi2_e1 o f). apply Ass1. apply Trans with (E_diese Thi2_D_E_fg (Epic_Equalizer_id (f:=Thi2_D_E_fg) Thi2_e1_RightInv) o Thi2_e1 o g). apply Comp_l. apply (Prf_E1_law1 Thi2_D_E_fg Elt1 Elt2). apply Ass. apply Trans with (Id Thi2_v o g). apply Comp_r; apply H2. apply Idl. Qed.
imports: Products1 Equalizers1 Single