let p be real number ; :: thesis:
reconsider p = p as Real by XREAL_0:def 1;
deffunc H₂( Element of REAL ) -> Element of REAL = $1 * (Re ((Sum (($1 * ) P_dt )) * ((cos . p) + ((sin . p) * ))));
consider Cr being Function of REAL ,REAL such that
A1: for th being Real holds Cr . th = H₂(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 )

let hy1 be convergent_to_0 Real_Sequence; :: thesis:
A3: for n being Element of NAT holds ((hy1 " ) (#) (Cr /* hy1)) . n = Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * )))

let n be Element of NAT ; :: thesis:
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) * (Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * ))))) by A1
.= (((hy1 . n) " ) * (hy1 . n)) * (Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * )))) ;
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 * (Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * )))) by A7, A9, XCMPLX_0:def 7
.= Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * ))) ;
thus ((hy1 " ) (#) (Cr /* hy1)) . n = Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * ))) by A10; :: thesis:

end;

deffunc H₃( Real) -> Element of REAL = Re ((Sum (((hy1 . $1) * ) P_dt )) * ((cos . p) + ((sin . p) * )));
consider rseq being Real_Sequence such that
A11: 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 )) * ((cos . p) + ((sin . p) * ));
consider cq1 being Complex_Sequence such that
A12: for n being Element of NAT holds cq1 . n = H₄(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

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

consider r being Real such that
A16: r > 0 and
A17: for z being complex number st |.z.| < r holds
|.(Sum (z P_dt )).| < q by A14, Th63;
A18: ( hy1 is convergent & lim hy1 = 0 ) by FDIFF_1:def 1;
consider k being Element of NAT such that
A19: for m being Element of NAT st k <= m holds
abs ((hy1 . m) - 0 ) < r by A16, A18, SEQ_2:def 7;

A20: now

end;

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

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:

end;

let n be Element of NAT ; :: thesis:
A30: (Re cq1) . n = Re (cq1 . n) by COMSEQ_3:def 3
.= Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * ))) by A12 ;
thus (Re cq1) . n = rseq . n by A11, A30; :: thesis:

end;

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

let n be Element of NAT ; :: thesis:
A32: rseq . n = Re ((Sum (((hy1 . n) * ) P_dt )) * ((cos . p) + ((sin . p) * ))) by A11;
thus rseq . n = ((hy1 " ) (#) (Cr /* hy1)) . n by A3, A32; :: thesis:

end;

end;

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

end;

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

take cos . p ; :: thesis:
thus for q being Real holds CL . q = (cos . p) * q by A36; :: thesis:

end;

reconsider PL = CL as LINEAR by A38, FDIFF_1:def 4;
A39: ex N being Neighbourhood of p st
( N c= dom sin & ( for r being Real st r in N holds
(sin . r) - (sin . p) = (PL . (r - p)) + (PR . (r - p)) ) )

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

let r be Real; :: thesis:
A41: r = p + (r - p) ;
A42: (sin . r) - (sin . p) = ((r - p) * (cos . p)) + ((r - p) * (Re ((Sum (((r - p) * ) P_dt )) * ((cos . p) + ((sin . p) * ))))) by A41, Th66
.= ((r - p) * (cos . p)) + (Cr . (r - p)) by A1
.= (PL . (r - p)) + (PR . (r - p)) by A36 ;
thus ( r in ].(p - 1),(p + 1).[ implies (sin . r) - (sin . p) = (PL . (r - p)) + (PR . (r - p)) ) by A42; :: thesis:

end;

take ].(p - 1),(p + 1).[ ; :: thesis:
thus ( ].(p - 1),(p + 1).[ is Neighbourhood of p & ].(p - 1),(p + 1).[ c= dom sin & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(sin . r) - (sin . p) = (PL . (r - p)) + (PR . (r - p)) ) ) by A40, Th27, RCOMP_1:def 7; :: thesis:

end;