proposition: Lemma Lp_coUAlaw2 : Limit_law2 (Limiting_cone l o_C G) Lp_diese.
proof: Proof. unfold Limit_law2, Limit_eq in |- *; simpl in |- *; intros d tau t. unfold Comp_cone_tau, Lp_diese in |- *. intro H'. apply Trans with (ApAphi la (ApAphi_inv la t)). apply Sym. apply (Idl_inv (NTa_areIso la (Build_POb1 d (Lim l))) t). apply AphiPres; apply (Prf_limit2 l). unfold Limit_eq in |- *; intro i. apply Trans with (ApAphi_inv la (t o FMor G (Limiting_cone l i))). apply Sym. apply (Adj_eq5 la (Limiting_cone l i) t). simpl in |- *; unfold Lp_sigma_tau in |- *; apply Aphi_invPres; apply (H' i). Qed.
imports: Adj_UA Pres_Limits