let p be Real; :: thesis: ( sin is_differentiable_in p & diff (sin,p) = cos . p )
reconsider p = p as Real ;
deffunc H₂( Real) -> Element of REAL = In (($1 * (Re ((Sum (($1 * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>))))),REAL);
consider Cr being Function of REAL,REAL such that
A1: for th being Element of REAL holds Cr . th = H₂(th) from FUNCT_2:sch 4();
for hy1 being non-zero 0 -convergent Real_Sequence holds
( (hy1 ") (#) (Cr /* hy1) is convergent & lim ((hy1 ") (#) (Cr /* hy1)) = 0 )

proof

let hy1 be non-zero 0 -convergent Real_Sequence; :: thesis: ( (hy1 ") (#) (Cr /* hy1) is convergent & lim ((hy1 ") (#) (Cr /* hy1)) = 0 )
A2: for n being Nat holds ((hy1 ") (#) (Cr /* hy1)) . n = Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))

proof

let n be Nat; :: thesis: ((hy1 ") (#) (Cr /* hy1)) . n = Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))
A3: n in NAT by ORDINAL1:def 12;
A4: ((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 A5: ((hy1 ") (#) (Cr /* hy1)) . n = ((hy1 . n) ") * (Cr . (hy1 . n)) by A4, FUNCT_2:108, A3
.= ((hy1 . n) ") * H₂(hy1 . n) by A1
.= (((hy1 . n) ") * (hy1 . n)) * (Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))) ;
hy1 . n <> 0 by SEQ_1:5;
then ((hy1 ") (#) (Cr /* hy1)) . n = 1 * (Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>)))) by A5, XCMPLX_0:def 7
.= Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>))) ;
hence ((hy1 ") (#) (Cr /* hy1)) . n = Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>))) ; :: thesis: verum

end;

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

proof

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

proof

consider r being Real such that
A10: r > 0 and
A11: for z being Complex st |.z.| < r holds
|.(Sum (z P_dt)).| < q by A9, Th57;
( hy1 is convergent & lim hy1 = 0 ) ;
then consider k being Nat such that
A12: for m being Nat st k <= m holds
|.((hy1 . m) - 0).| < r by A10, SEQ_2:def 7;

A13: now :: thesis: for m being Nat st k <= m holds
|.((cq1 . m) - 0c).| < q

let m be Nat; :: thesis: ( k <= m implies |.((cq1 . m) - 0c).| < q )
assume A14: k <= m ; :: thesis: |.((cq1 . m) - 0c).| < q
A15: |.((cq1 . m) - 0c).| = |.((Sum (((hy1 . m) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>))).| by A7
.= |.(Sum (((hy1 . m) * <i>) P_dt)).| * |.((cos . p) + ((sin . p) * <i>)).| by COMPLEX1:65
.= |.(Sum (((hy1 . m) * <i>) P_dt)).| * |.(Sum ((p * <i>) ExpSeq)).| by Lm3
.= |.(Sum (((hy1 . m) * <i>) P_dt)).| * 1 by Lm5
.= |.(Sum (((hy1 . m) * <i>) P_dt)).| ;
A16: |.((hy1 . m) - 0).| < r by A12, A14;
(hy1 . m) * <i> = 0 + ((hy1 . m) * <i>) ;
then ( Re ((hy1 . m) * <i>) = 0 & Im ((hy1 . m) * <i>) = hy1 . m ) by COMPLEX1:12;
then |.((hy1 . m) * <i>).| = |.(hy1 . m).| by COMPLEX1:72;
hence |.((cq1 . m) - 0c).| < q by A11, A15, A16; :: thesis: verum

end;

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

end;

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

end;

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

proof

let n be Element of NAT ; :: thesis: (Re cq1) . n = rseq . n
(Re cq1) . n = Re (cq1 . n) by COMSEQ_3:def 5
.= Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>))) by A7 ;
hence (Re cq1) . n = rseq . n by A6; :: 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 = Re ((Sum (((hy1 . n) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>))) by A6;
hence rseq . n = ((hy1 ") (#) (Cr /* hy1)) . n by A2; :: thesis: verum

end;

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

end;

then reconsider PR = Cr as RestFunc by FDIFF_1:def 2;
deffunc H₃( Real) -> Element of REAL = In (($1 * (cos . p)),REAL);
consider CL being Function of REAL,REAL such that
A20: for th being Element of REAL holds CL . th = H₃(th) from FUNCT_2:sch 4();
A21: for d being Real holds CL . d = d * (cos . p)

proof

let d be Real; :: thesis: CL . d = d * (cos . p)
d in REAL by XREAL_0:def 1;
then CL . d = H₃(d) by A20;
hence CL . d = d * (cos . p) ; :: thesis: verum

end;

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

proof

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

end;

then reconsider PL = CL as LinearFunc by FDIFF_1:def 3;
A22: 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)) ) )

proof

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

proof

let r be Real; :: thesis: ( r in ].(p - 1),(p + 1).[ implies (sin . r) - (sin . p) = (PL . (r - p)) + (PR . (r - p)) )
A24: r - p in REAL by XREAL_0:def 1;
r = p + (r - p) ;
then (sin . r) - (sin . p) = ((r - p) * (cos . p)) + ((r - p) * (Re ((Sum (((r - p) * <i>) P_dt)) * ((cos . p) + ((sin . p) * <i>))))) by Th60
.= ((r - p) * (cos . p)) + H₂(r - p)
.= ((r - p) * (cos . p)) + (Cr . (r - p)) by A1, A24
.= (PL . (r - p)) + (PR . (r - p)) by A21 ;
hence ( r in ].(p - 1),(p + 1).[ implies (sin . r) - (sin . 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 sin & ( for r being Real st r in ].(p - 1),(p + 1).[ holds
(sin . r) - (sin . p) = (PL . (r - p)) + (PR . (r - p)) ) )
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 A23, Th24, RCOMP_1:def 6; :: thesis: verum

end;

then A25: sin is_differentiable_in p by FDIFF_1:def 4;
PL . 1 = 1 * (cos . p) by A21;
hence ( sin is_differentiable_in p & diff (sin,p) = cos . p ) by A22, A25, FDIFF_1:def 5; :: thesis: verum