proposition: Lemma Thl_diag4 : Thl_h o Thl_f =_S Thl_h o Thl_g.
proof: Proof. apply Trans with (Pd1_diese Thl_l_Fu (c:=c) (fun u : Arrs J => tau (Codom u))). apply (Prf_pd1_law2 (l:=Thl_l_Fu) (r:=c) (h:=fun u : Arrs J => tau (Codom u))). unfold Product_eq in |- *; intro u. apply Trans with (Thl_h o Proj1 Thl_l_Fi (Codom u)). apply (Thl_diag3 (Codom u)). apply Trans with (Thl_h o Thl_f o Proj1 Thl_l_Fu u). apply Comp_l. apply (Thl_diag1 u). apply Ass. apply Sym. apply (Prf_pd1_law2 (l:=Thl_l_Fu) (r:=c) (h:=fun u : Arrs J => tau (Codom u))). unfold Product_eq in |- *; intro u. apply Trans with (tau (Dom u) o FMor F (Arrow u)). apply (Eq_cone tau (Arrow u)). apply Trans with ((Thl_h o Proj1 Thl_l_Fi (Dom u)) o FMor F (Arrow u)). apply Comp_r. apply (Thl_diag3 (Dom u)). apply Trans with (Thl_h o Proj1 Thl_l_Fi (Dom u) o FMor F (Arrow u)). apply Ass1. apply Trans with (Thl_h o Thl_g o Proj1 Thl_l_Fu u). apply Comp_l. apply (Thl_diag2 u). apply Ass. Qed.
imports: Equalizers1 Products1