proposition: Lemma E_monic : Monic_law (E_mor f).
proof: Proof. unfold Monic_law in |- *; intros c j l H. cut (Equalizer_eq (j o E_mor f)). intro p. apply Trans with (E_diese f p). apply (Prf_E_law3 p (l:=j)). apply Refl. apply Sym; apply (Prf_E_law3 p (l:=l)). apply H. unfold Equalizer_eq in |- *; intros i1 i2. apply Trans with (j o E_mor f o k i1). apply Ass1. apply Trans with (j o E_mor f o k i2). apply Comp_l; apply (Prf_E_law1 f i1 i2). apply Ass. Qed.
imports: CatProperty