proposition: Lemma Prf_law1_fg : forall (r : C) (h : r --> a), h o f =_S h o g -> Equalizer_eq K_fg h.
proof: Proof. intros r h H; unfold Equalizer_eq in |- *. intros i j; elim i; elim j; simpl in |- *. apply Refl. apply H. apply Sym; trivial. apply Refl. Qed.
imports: Equalizers PA Limit