let p be real number ; :: thesis: ( exp_R is_differentiable_in p & diff exp_R ,p = exp_R . p )
deffunc H2( 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 = H2(th) from FUNCT_2:sch 4();
 A2: 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 )
A3: 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 )))
A4: ((hy1 " ) (#) (Cr /* hy1)) . n = ((hy1 " ) . n) * ((Cr /* hy1) . n) by SEQ_1:12
.= ((hy1 . n) " ) * ((Cr /* hy1) . n) by VALUED_1:10 ;
A5: dom Cr = REAL by FUNCT_2:def 1;
A6: rng hy1 c= dom Cr by A5;
A7: ((hy1 " ) (#) (Cr /* hy1)) . n = ((hy1 . n) " ) * (Cr . (hy1 . n)) by A4, A6, FUNCT_2:185
.= ((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 )))) ;
A8: hy1 is non-empty by FDIFF_1:def 1;
A9: hy1 . n <> 0 by A8, SEQ_1:7;
A10: ((hy1 " ) (#) (Cr /* hy1)) . n = 1 * ((exp_R . p) * (Re (Sum ((hy1 . n) P_dt )))) by A7, A9, XCMPLX_0:def 7
.= (exp_R . p) * (Re (Sum ((hy1 . n) P_dt ))) ;
thus ((hy1 " ) (#) (Cr /* hy1)) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt ))) by A10; :: thesis: verum
end;
deffunc H3( Real) -> Element of REAL = (exp_R . p) * (Re (Sum ((hy1 . $1) P_dt )));
consider rseq being Real_Sequence such that
A11: for n being Element of NAT holds rseq . n = H3(n) from SEQ_1:sch 1();
 deffunc H4( Element of NAT ) -> Element of COMPLEX = (Sum ((hy1 . $1) P_dt )) * (exp_R . p);
consider cq1 being Complex_Sequence such that
A12: for n being Element of NAT holds cq1 . n = H4(n) from COMSEQ_1:sch 1();
 A13: 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 A14: q > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q
A15: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q
proof
A16: exp_R . p > 0 by Th59;
consider r being Real such that
A17: r > 0 and
A18: for z being complex number st |.z.| < r holds
|.(Sum (z P_dt )).| < q / (exp_R . p) by A14, A16, Th63;
A19: ( hy1 is convergent & lim hy1 = 0 ) by FDIFF_1:def 1;
consider k being Element of NAT such that
A20: for m being Element of NAT st k <= m holds
abs ((hy1 . m) - 0 ) < r by A17, A19, SEQ_2:def 7;
A21: now
let m be Element of NAT ; :: thesis: ( k <= m implies |.((cq1 . m) - 0c ).| < q )
assume A22: k <= m ; :: thesis: |.((cq1 . m) - 0c ).| < q
A23: |.((cq1 . m) - 0c ).| = |.((Sum ((hy1 . m) P_dt )) * (exp_R . p)).| by A12
.= |.(Sum ((hy1 . m) P_dt )).| * |.(exp_R . p).| by COMPLEX1:151
.= |.(Sum ((hy1 . m) P_dt )).| * (sqrt (((Re (exp_R . p)) ^2 ) + ((Im (exp_R . p)) ^2 ))) ;
A24: exp_R . p = (exp_R . p) + (0 * <i> ) ;
A25: ( Re (exp_R . p) = exp_R . p & Im (exp_R . p) = 0 ) by A24, COMPLEX1:28;
A26: exp_R . p > 0 by Th59;
A27: |.((cq1 . m) - 0c ).| = |.(Sum ((hy1 . m) P_dt )).| * (exp_R . p) by A23, A25, A26, SQUARE_1:89;
A28: abs ((hy1 . m) - 0 ) < r by A20, A22;
A29: |.((cq1 . m) - 0c ).| < (q / (exp_R . p)) * (exp_R . p) by A18, A26, A27, A28, XREAL_1:70;
thus |.((cq1 . m) - 0c ).| < q by A26, A29, XCMPLX_1:88; :: 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 A21; :: thesis: verum
end;
thus ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((cq1 . m) - 0c ).| < q by A15; :: thesis: verum
end;
A30: cq1 is convergent by A13, COMSEQ_2:def 4;
A31: lim cq1 = 0c by A13, A30, COMSEQ_2:def 5;
A32: for n being Element of NAT holds (Re cq1) . n = rseq . n
proof
A33: 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 )))
A34: (Re cq1) . n = Re (cq1 . n) by COMSEQ_3:def 3
.= Re ((Sum ((hy1 . n) P_dt )) * (exp_R . p)) by A12
.= (exp_R . p) * (Re (Sum ((hy1 . n) P_dt ))) by Lm13 ;
thus (Re cq1) . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt ))) by A34; :: thesis: verum
end;
let n be Element of NAT ; :: thesis: (Re cq1) . n = rseq . n
A35: rseq . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt ))) by A11;
thus (Re cq1) . n = rseq . n by A33, A35; :: thesis: verum
end;
A36: 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
A37: rseq . n = (exp_R . p) * (Re (Sum ((hy1 . n) P_dt ))) by A11;
thus rseq . n = ((hy1 " ) (#) (Cr /* hy1)) . n by A3, A37; :: thesis: verum
end;
A38: rseq = (hy1 " ) (#) (Cr /* hy1) by A36, FUNCT_2:113;
A39: (hy1 " ) (#) (Cr /* hy1) = Re cq1 by A32, A38, FUNCT_2:113;
thus ( (hy1 " ) (#) (Cr /* hy1) is convergent & lim ((hy1 " ) (#) (Cr /* hy1)) = 0 ) by A30, A31, A39, COMPLEX1:12, COMSEQ_3:41; :: thesis: verum
end;
reconsider PR = Cr as REST by A2, FDIFF_1:def 3;
deffunc H3( Element of REAL ) -> Element of REAL = $1 * (exp_R . p);
consider CL being Function of REAL ,REAL such that
A40: for th being Real holds CL . th = H3(th) from FUNCT_2:sch 4();
 A41: 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)
A42: d is Real by XREAL_0:def 1;
thus CL . d = d * (exp_R . p) by A40, A42; :: thesis: verum
end;
A43: 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 A41; :: thesis: verum
end;
reconsider PL = CL as LINEAR by A43, FDIFF_1:def 4;
A44: 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
A45: 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;
A46: r = p + (r - p) ;
A47: (exp_R . r) - (exp_R . p) = ((r - p) * (exp_R . p)) + (((r - p) * (exp_R . p)) * (Re (Sum ((r - p) P_dt )))) by A46, Th67
.= ((r - p) * (exp_R . p)) + (Cr . (r - p)) by A1
.= (PL . (r - p)) + (PR . (r - p)) by A41 ;
thus ( r in ].(p - 1),(p + 1).[ implies (exp_R . r) - (exp_R . p) = (PL . (r - p)) + (PR . (r - p)) ) by A47; :: 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 A45, Th51, RCOMP_1:def 7; :: thesis: verum
end;
A48: exp_R is_differentiable_in p by A44, FDIFF_1:def 5;
A49: PL . 1 = 1 * (exp_R . p) by A41;
thus ( exp_R is_differentiable_in p & diff exp_R ,p = exp_R . p ) by A44, A48, A49, FDIFF_1:def 6; :: thesis: verum