proposition: Lemma Thi2_e1_RightInv : RIso_law Thi2_e1 (Thi2_e o Thi2_s).
proof: Proof. unfold RIso_law in |- *; simpl in |- *. apply Trans with (Thi2_e o Thi2_s o Thi2_e1). apply Ass1. apply (E_monic (f:=Thi2_D_E_hom)). simpl in |- *. apply Trans with (Thi2_e o (Thi2_s o Thi2_e1) o Thi2_e). apply Ass1. apply Trans with (Thi2_e o Id Thi2_w). apply (Prf_E1_law1 Thi2_D_E_hom ((Thi2_s o Thi2_e1) o Thi2_e) (Id Thi2_w)). apply Trans with Thi2_e. apply Idr1. apply Idl1. Qed.
imports: Products1 Equalizers1 Single