proposition: Lemma Tc_t_cone_com_law : Com_law (axf:=axf) (bxg:=Tc_limF) (Lim_diese l_F' Tc_t_cone).
proof: Proof. unfold Com_law in |- *; unfold Mor_com_ob at 1 in |- *; simpl in |- *. apply Sym; apply (Prf_limit2 l_GF'). unfold Limit_eq in |- *; simpl in |- *; intro i. apply Trans with (Mor_com_ob axf o FMor G (Lim_diese l_F' Tc_t_cone) o FMor G (Limiting_cone l_F' i)). apply Ass1. apply Trans with (Mor_com_ob axf o FMor G (Tc_t_tau i)). apply Comp_l. apply Trans with (FMor G (Lim_diese l_F' Tc_t_cone o Limiting_cone l_F' i)). apply FComp1. unfold FMor in |- *; apply (Pres (FMap G (Ob_com_ob axf) (Ob_com_ob (F i)))). apply (Prf_limit1 l_F' Tc_t_cone i). apply Sym; apply (Prf_com_law (t i)). Qed.
imports: Pres_Limits Comma_proj