let p be real number ; :: thesis: ( exp_R is_differentiable_in p & diff (exp_R,p) = exp_R . p )
deffunc H₂( Element of REAL ) -> Element of REAL = ($1 * (exp_R . p)) * (Re (Sum ($1 P_dt)));
consider Cr being Function of REAL,REAL such that
A1: for th being Real holds Cr . th = H₂(th) from FUNCT_2:sch 4();
for hy1 being convergent_to_0 Real_Sequence holds
( (hy1 ") (#) (Cr /* hy1) is convergent & lim ((hy1 ") (#) (Cr /* hy1)) = 0 )

proof

let hy1 be convergent_to_0 Real_Sequence; :: thesis: ( (hy1 ") (#) (Cr /* hy1) is convergent & lim ((hy1 ") (#) (Cr /* hy1)) = 0 )
A2: for n being Element of NAT holds ((hy1 ") (#) (Cr /* hy1)) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt)))

proof

let n be Element of NAT ; :: thesis: ((hy1 ") (#) (Cr /* hy1)) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt)))
A3: ((hy1 ") (#) (Cr /* hy1)) . n = ((hy1 ") . n) * ((Cr /* hy1) . n) by SEQ_1:8
.= ((hy1 . n) ") * ((Cr /* hy1) . n) by VALUED_1:10 ;
dom Cr = REAL by FUNCT_2:def 1;
then rng hy1 c= dom Cr ;
then A4: ((hy1 ") (#) (Cr /* hy1)) . n = ((hy1 . n) ") * (Cr . (hy1 . n)) by A3, FUNCT_2:108
.= ((hy1 . n) ") * (((hy1 . n) * (exp_R . p)) * (Re (Sum ((hy1 . n) P_dt)))) by A1
.= (((hy1 . n) ") * (hy1 . n)) * ((exp_R . p) * (Re (Sum ((hy1 . n) P_dt)))) ;
hy1 is non-empty by FDIFF_1:def 1;
then hy1 . n <> 0 by SEQ_1:5;
then ((hy1 ") (#) (Cr /* hy1)) . n = 1 * ((exp_R . p) * (Re (Sum ((hy1 . n) P_dt)))) by A4, XCMPLX_0:def 7
.= (exp_R . p) * (Re (Sum ((hy1 . n) P_dt))) ;
hence ((hy1 ") (#) (Cr /* hy1)) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt))) ; :: thesis: verum

end;

deffunc H₃( Real) -> Element of REAL = (exp_R . p) * (Re (Sum ((hy1 . $1) P_dt)));
consider rseq being Real_Sequence such that
A5: for n being Element of NAT holds rseq . n = H₃(n) from SEQ_1:sch 1();
deffunc H₄( Element of NAT ) -> Element of COMPLEX = (Sum ((hy1 . $1) P_dt)) * (exp_R . p);
consider cq1 being Complex_Sequence such that
A6: for n being Element of NAT holds cq1 . n = H₄(n) from COMSEQ_1:sch 1();
A7: for q being Real st q > 0 holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c).| < q

proof

let q be Real; :: thesis: ( q > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c).| < q )
assume A8: q > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c).| < q
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c).| < q

proof

exp_R . p > 0 by Th59;
then consider r being Real such that
A9: r > 0 and
A10: for z being complex number st |.z.| < r holds
|.(Sum (z P_dt)).| < q / (exp_R . p) by A8, Th63;
( hy1 is convergent & lim hy1 = 0 ) by FDIFF_1:def 1;
then consider k being Element of NAT such that
A11: for m being Element of NAT st k <= m holds
abs ((hy1 . m) - 0) < r by A9, SEQ_2:def 7;

A12: now

let m be Element of NAT ; :: thesis: ( k <= m implies |.((cq1 . m) - 0c).| < q )
assume A13: k <= m ; :: thesis: |.((cq1 . m) - 0c).| < q
A14: |.((cq1 . m) - 0c).| = |.((Sum ((hy1 . m) P_dt)) * (exp_R . p)).| by A6
.= |.(Sum ((hy1 . m) P_dt)).| * |.(exp_R . p).| by COMPLEX1:65
.= |.(Sum ((hy1 . m) P_dt)).| * (sqrt (((Re (exp_R . p)) ^2) + ((Im (exp_R . p)) ^2))) ;
exp_R . p = (exp_R . p) + (0 * <i>) ;
then A15: ( Re (exp_R . p) = exp_R . p & Im (exp_R . p) = 0 ) by COMPLEX1:12;
A16: exp_R . p > 0 by Th59;
then A17: |.((cq1 . m) - 0c).| = |.(Sum ((hy1 . m) P_dt)).| * (exp_R . p) by A14, A15, SQUARE_1:22;
abs ((hy1 . m) - 0) < r by A11, A13;
then |.((cq1 . m) - 0c).| < (q / (exp_R . p)) * (exp_R . p) by A10, A16, A17, XREAL_1:68;
hence |.((cq1 . m) - 0c).| < q by A16, XCMPLX_1:87; :: thesis: verum

end;

take k ; :: thesis: for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c).| < q
thus for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c).| < q by A12; :: thesis: verum

end;

hence ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c).| < q ; :: thesis: verum

end;

then A18: cq1 is convergent by COMSEQ_2:def 4;
then A19: lim cq1 = 0c by A7, COMSEQ_2:def 5;
A20: for n being Element of NAT holds (Re cq1) . n = rseq . n

proof

A21: for n being Element of NAT holds (Re cq1) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt)))

proof

let n be Element of NAT ; :: thesis: (Re cq1) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt)))
(Re cq1) . n = Re (cq1 . n) by COMSEQ_3:def 5
.= Re ((Sum ((hy1 . n) P_dt)) * (exp_R . p)) by A6
.= (exp_R . p) * (Re (Sum ((hy1 . n) P_dt))) by Lm12 ;
hence (Re cq1) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt))) ; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: (Re cq1) . n = rseq . n
rseq . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt))) by A5;
hence (Re cq1) . n = rseq . n by A21; :: thesis: verum

end;

for n being Element of NAT holds rseq . n = ((hy1 ") (#) (Cr /* hy1)) . n

proof

let n be Element of NAT ; :: thesis: rseq . n = ((hy1 ") (#) (Cr /* hy1)) . n
rseq . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt))) by A5;
hence rseq . n = ((hy1 ") (#) (Cr /* hy1)) . n by A2; :: thesis: verum

end;

then rseq = (hy1 ") (#) (Cr /* hy1) by FUNCT_2:63;
then (hy1 ") (#) (Cr /* hy1) = Re cq1 by A20, FUNCT_2:63;
hence ( (hy1 ") (#) (Cr /* hy1) is convergent & lim ((hy1 ") (#) (Cr /* hy1)) = 0 ) by A18, A19, COMPLEX1:4, COMSEQ_3:41; :: thesis: verum

end;

then reconsider PR = Cr as REST by FDIFF_1:def 2;
deffunc H₃( Element of REAL ) -> Element of REAL = $1 * (exp_R . p);
consider CL being Function of REAL,REAL such that
A22: for th being Real holds CL . th = H₃(th) from FUNCT_2:sch 4();
A23: for d being real number holds CL . d = d * (exp_R . p)

proof

let d be real number ; :: thesis: CL . d = d * (exp_R . p)
d is Real by XREAL_0:def 1;
hence CL . d = d * (exp_R . p) by A22; :: thesis: verum

end;

ex r being Real st
for q being Real holds CL . q = r * q

proof

take exp_R . p ; :: thesis: for q being Real holds CL . q = (exp_R . p) * q
thus for q being Real holds CL . q = (exp_R . p) * q by A23; :: thesis: verum

end;

then reconsider PL = CL as LINEAR by FDIFF_1:def 3;
A24: ex N being Neighbourhood of p st
( N c= dom exp_R & ( for r being Real st r in N holds
(exp_R . r) - (exp_R . p) = (PL . (r - p)) + (PR . (r - p)) ) )

proof

A25: for r being Real st r in ].(p - 1),(p + 1).[ holds
(exp_R . r) - (exp_R . p) = (PL . (r - p)) + (PR . (r - p))

proof

let r be Real; :: thesis: ( r in ].(p - 1),(p + 1).[ implies (exp_R . r) - (exp_R . p) = (PL . (r - p)) + (PR . (r - p)) )
reconsider p = p as Real by XREAL_0:def 1;
r = p + (r - p) ;
then (exp_R . r) - (exp_R . p) = ((r - p) * (exp_R . p)) + (((r - p) * (exp_R . p)) * (Re (Sum ((r - p) P_dt)))) by Th67
.= ((r - p) * (exp_R . p)) + (Cr . (r - p)) by A1
.= (PL . (r - p)) + (PR . (r - p)) by A23 ;
hence ( r in ].(p - 1),(p + 1).[ implies (exp_R . r) - (exp_R . p) = (PL . (r - p)) + (PR . (r - p)) ) ; :: thesis: verum

end;

take ].(p - 1),(p + 1).[ ; :: thesis: ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom exp_R & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(exp_R . r) - (exp_R . p) = (PL . (r - p)) + (PR . (r - p)) ) )
thus ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom exp_R & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(exp_R . r) - (exp_R . p) = (PL . (r - p)) + (PR . (r - p)) ) ) by A25, Th51, RCOMP_1:def 6; :: thesis: verum

end;

then A26: exp_R is_differentiable_in p by FDIFF_1:def 4;
PL . 1 = 1 * (exp_R . p) by A23;
hence ( exp_R is_differentiable_in p & diff (exp_R,p) = exp_R . p ) by A24, A26, FDIFF_1:def 5; :: thesis: verum