proposition: Lemma Exp_unique : forall F, Derivative realline I F F -> (forall H1, F [0] H1 [=] [1]) -> Feq realline Expon F.
proof: Proof. intros F H H0. cut (forall n : nat, Derivative_n n realline I Expon Expon). intro derF. cut (Taylor_bnd (fun n : nat => Expon)); [ intro bndf | apply Exp_bnd ]. cut (forall n : nat, Derivative_n n realline I F F). intros derG. apply Taylor_unique_crit with (f := fun _ : nat => Expon) (a := ZeroR) (g := fun n : nat => F) (bndf := bndf) (derF := derF); auto. apply bnd_imp_Taylor_bnd with F. intros; apply eq_imp_leEq; algebra. apply Derivative_n_imp_Continuous with I 1 F; auto with arith. intro n. change (included realline (Dom F)) in |- *. apply Derivative_n_imp_inc with I 1 F; auto with arith. intros; astepr OneR. astepr (Exp [0]). Opaque Expon. unfold Exp in |- *; simpl in |- *; algebra. Transparent Expon. apply Taylor_Series_conv_to_fun; auto. apply Exp_unique_lemma; auto. apply Exp_unique_lemma; apply Derivative_Exp. Qed.
imports: CoRN.transc.TaylorSeries