proposition: Lemma tech12 : forall (An:nat -> R) (x l:R), Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l -> Pser An x l.
proof: Proof. intros; unfold Pser; unfold infinite_sum; unfold Un_cv in H; assumption. Qed.
imports: Rbase Rfunctions Rseries Rcomplete