proposition: Lemma Prf_pd1_law2 : Product_law2 Proj1 Pd1_diese.
proof: Proof. unfold Product_law2, Product_eq in |- *; intros c f g H. unfold Pd1_diese in |- *; apply (Prf_limit2 l). unfold Limit_eq in |- *; simpl in |- *; unfold Product_tau in |- *; simpl in |- *. intro i; apply Sym; apply (H i). Qed.
imports: Limit Discr Products