proposition: Lemma Taylor_unique_crit : Feq realline F (FSeries_Sum Hf) -> Feq realline F G.
proof: Proof. intro H. cut (fun_series_convergent_IR realline (Taylor_Series realline I G a I g derG)). intro Hg. apply Feq_transitive with (FSeries_Sum Hf); auto. apply Feq_transitive with (FSeries_Sum Hg). apply eq_imp_Feq; simpl in |- *; Included. intros; apply series_sum_wd. intros; algebra. apply Feq_symmetric; apply Taylor_Series_conv_to_fun; auto. apply Taylor_Series_conv_IR; auto. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor