let n be Element of NAT ; :: thesis: for th being Real holds
( (Partial_Sums (th P_sin )) . n = (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * n) + 1) & (Partial_Sums (th P_cos )) . n = (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * n) )
let th be Real; :: thesis: ( (Partial_Sums (th P_sin )) . n = (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * n) + 1) & (Partial_Sums (th P_cos )) . n = (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * n) )

A1: now

A2: (Partial_Sums (th P_sin )) . 0 = (th P_sin ) . 0 by SERIES_1:def 1
.= (((- 1) |^ 0 ) * (th |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! ) by Def24 ;
A3: th |^ ((2 * 0 ) + 1) = (th GeoSeq ) . (0 + 1) by PREPOWER:def 1
.= ((th GeoSeq ) . 0 ) * th by PREPOWER:4
.= 1 * th by PREPOWER:4
.= th ;
A4: ((2 * 0 ) + 1) ! = (0 ! ) * 1 by NEWTON:21
.= 1 by NEWTON:18 ;
A5: (- 1) |^ 0 = ((- 1) GeoSeq ) . 0 by PREPOWER:def 1
.= 1 by PREPOWER:4 ;
A6: (Partial_Sums (th P_cos )) . 0 = (th P_cos ) . 0 by SERIES_1:def 1
.= (((- 1) |^ 0 ) * (th |^ (2 * 0 ))) / ((2 * 0 ) ! ) by Def25
.= (1 * ((th GeoSeq ) . 0 )) / 1 by A5, NEWTON:18, PREPOWER:def 1
.= 1 by PREPOWER:4 ;
A7: ( (Im ((th * <i> ) ExpSeq )) . 0 = Im (((th * <i> ) ExpSeq ) . 0 ) & (Im ((th * <i> ) ExpSeq )) . 1 = Im (((th * <i> ) ExpSeq ) . 1) ) by COMSEQ_3:def 4;
A8: th * <i> = 0 + (th * <i> ) ;
A9: (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * 0 ) + 1) = ((Partial_Sums (Im ((th * <i> ) ExpSeq ))) . 0 ) + ((Im ((th * <i> ) ExpSeq )) . 1) by SERIES_1:def 1
.= ((Im ((th * <i> ) ExpSeq )) . 0 ) + ((Im ((th * <i> ) ExpSeq )) . 1) by SERIES_1:def 1
.= 0 + (Im (((th * <i> ) ExpSeq ) . (0 + 1))) by A7, Th4, COMPLEX1:15
.= 0 + (Im (((((th * <i> ) ExpSeq ) . 0 ) * (th * <i> )) / ((0 + 1) + (0 * <i> )))) by Th4
.= Im ((1 * (th * <i> )) / 1) by Th4
.= th by A8, COMPLEX1:28 ;
defpred S₁[ Element of NAT ] means ( (Partial_Sums (th P_sin )) . $1 = (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * $1) + 1) & (Partial_Sums (th P_cos )) . $1 = (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * $1) );
A10: (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * 0 ) = (Re ((th * <i> ) ExpSeq )) . 0 by SERIES_1:def 1
.= Re (((th * <i> ) ExpSeq ) . 0 ) by COMSEQ_3:def 3
.= 1 by Th4, COMPLEX1:15 ;
A11: S₁[ 0 ] by A2, A3, A4, A5, A6, A9, A10;
A12: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A13: (Partial_Sums (th P_sin )) . k = (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * k) + 1) and
A14: (Partial_Sums (th P_cos )) . k = (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * k) ; :: thesis: S₁[k + 1]
A15: (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (Im ((th * <i> ) ExpSeq ))) . (((2 * k) + 1) + 1)) + ((Im ((th * <i> ) ExpSeq )) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_sin )) . k) + ((Im ((th * <i> ) ExpSeq )) . (2 * (k + 1)))) + ((Im ((th * <i> ) ExpSeq )) . ((2 * (k + 1)) + 1)) by A13, SERIES_1:def 1
.= (((Partial_Sums (th P_sin )) . k) + (Im (((th * <i> ) ExpSeq ) . (2 * (k + 1))))) + ((Im ((th * <i> ) ExpSeq )) . ((2 * (k + 1)) + 1)) by COMSEQ_3:def 4
.= (((Partial_Sums (th P_sin )) . k) + (Im (((th * <i> ) ExpSeq ) . (2 * (k + 1))))) + (Im (((th * <i> ) ExpSeq ) . ((2 * (k + 1)) + 1))) by COMSEQ_3:def 4
.= (((Partial_Sums (th P_sin )) . k) + (Im (((th * <i> ) |^ (2 * (k + 1))) / ((2 * (k + 1)) !c )))) + (Im (((th * <i> ) ExpSeq ) . ((2 * (k + 1)) + 1))) by Def8
.= (((Partial_Sums (th P_sin )) . k) + (Im (((th * <i> ) |^ (2 * (k + 1))) / ((2 * (k + 1)) !c )))) + (Im (((th * <i> ) |^ ((2 * (k + 1)) + 1)) / (((2 * (k + 1)) + 1) !c ))) by Def8
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !c )))) + (Im (((th * <i> ) |^ ((2 * (k + 1)) + 1)) / (((2 * (k + 1)) + 1) !c ))) by Th36
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !c )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) !c ))) by Th36
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) !c ))) by Th37
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) ! ))) by Th37
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !c )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) ! ))) by Th37
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !c )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) !c ))) by Th37
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) !c ))) by Th37
.= (((Partial_Sums (th P_sin )) . k) + (Im ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) ! ))) by Th37 ;
A16: (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * (k + 1)) + 1) = (((Partial_Sums (th P_sin )) . k) + (Im (((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )) + ((0 / ((2 * (k + 1)) ! )) * <i> )))) + (Im (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) * <i> ) / (((2 * (k + 1)) + 1) ! ))) by A15;
A17: (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * (k + 1)) + 1) = (((Partial_Sums (th P_sin )) . k) + 0 ) + (Im ((0 / (((2 * (k + 1)) + 1) ! )) + (((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) / (((2 * (k + 1)) + 1) ! )) * <i> ))) by A16, COMPLEX1:28
.= (((Partial_Sums (th P_sin )) . k) + (0 / ((2 * (k + 1)) ! ))) + ((((- 1) |^ (k + 1)) * (th |^ ((2 * (k + 1)) + 1))) / (((2 * (k + 1)) + 1) ! )) by COMPLEX1:28 ;
A18: (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * (k + 1)) + 1) = ((Partial_Sums (th P_sin )) . k) + ((th P_sin ) . (k + 1)) by A17, Def24
.= (Partial_Sums (th P_sin )) . (k + 1) by SERIES_1:def 1 ;
A19: (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * (k + 1)) = ((Partial_Sums (Re ((th * <i> ) ExpSeq ))) . ((2 * k) + 1)) + ((Re ((th * <i> ) ExpSeq )) . (((2 * k) + 1) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_cos )) . k) + ((Re ((th * <i> ) ExpSeq )) . ((2 * k) + 1))) + ((Re ((th * <i> ) ExpSeq )) . (((2 * k) + 1) + 1)) by A14, SERIES_1:def 1
.= (((Partial_Sums (th P_cos )) . k) + (Re (((th * <i> ) ExpSeq ) . ((2 * k) + 1)))) + ((Re ((th * <i> ) ExpSeq )) . (((2 * k) + 1) + 1)) by COMSEQ_3:def 3
.= (((Partial_Sums (th P_cos )) . k) + (Re (((th * <i> ) ExpSeq ) . ((2 * k) + 1)))) + (Re (((th * <i> ) ExpSeq ) . (((2 * k) + 1) + 1))) by COMSEQ_3:def 3
.= (((Partial_Sums (th P_cos )) . k) + (Re (((th * <i> ) |^ ((2 * k) + 1)) / (((2 * k) + 1) !c )))) + (Re (((th * <i> ) ExpSeq ) . (((2 * k) + 1) + 1))) by Def8
.= (((Partial_Sums (th P_cos )) . k) + (Re (((th * <i> ) |^ ((2 * k) + 1)) / (((2 * k) + 1) !c )))) + (Re (((th * <i> ) |^ (2 * (k + 1))) / ((((2 * k) + 1) + 1) !c ))) by Def8
.= (((Partial_Sums (th P_cos )) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ) / (((2 * k) + 1) !c )))) + (Re (((th * <i> ) |^ (2 * (k + 1))) / ((2 * (k + 1)) !c ))) by Th36
.= (((Partial_Sums (th P_cos )) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ) / (((2 * k) + 1) !c )))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !c ))) by Th36
.= (((Partial_Sums (th P_cos )) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ) / (((2 * k) + 1) ! )))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) !c ))) by Th37
.= (((Partial_Sums (th P_cos )) . k) + (Re (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) * <i> ) / (((2 * k) + 1) ! )))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! ))) by Th37 ;
A20: (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * (k + 1)) = (((Partial_Sums (th P_cos )) . k) + (Re ((0 / (((2 * k) + 1) ! )) + (((((- 1) |^ k) * (th |^ ((2 * k) + 1))) / (((2 * k) + 1) ! )) * <i> )))) + (Re ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! ))) by A19;
A21: (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * (k + 1)) = (((Partial_Sums (th P_cos )) . k) + (0 / (((2 * k) + 1) ! ))) + (Re (((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )) + ((0 / ((2 * (k + 1)) ! )) * <i> ))) by A20, COMPLEX1:28
.= (((Partial_Sums (th P_cos )) . k) + (0 / (((2 * k) + 1) ! ))) + ((((- 1) |^ (k + 1)) * (th |^ (2 * (k + 1)))) / ((2 * (k + 1)) ! )) by COMPLEX1:28 ;
A22: (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * (k + 1)) = ((Partial_Sums (th P_cos )) . k) + ((th P_cos ) . (k + 1)) by A21, Def25
.= (Partial_Sums (th P_cos )) . (k + 1) by SERIES_1:def 1 ;
thus S₁[k + 1] by A18, A22; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A11, A12); :: thesis: verum

end;

thus ( (Partial_Sums (th P_sin )) . n = (Partial_Sums (Im ((th * <i> ) ExpSeq ))) . ((2 * n) + 1) & (Partial_Sums (th P_cos )) . n = (Partial_Sums (Re ((th * <i> ) ExpSeq ))) . (2 * n) ) by A1; :: thesis: verum