let th be Real; :: thesis: (Sum ((th * <i> ) ExpSeq )) *' = Sum ((- (th * <i> )) ExpSeq )
(Partial_Sums ((th * <i> ) ExpSeq )) *' = Partial_Sums ((- (th * <i> )) ExpSeq )

proof

A1: for n being Element of NAT holds (((th * <i> ) ExpSeq ) . n) *' = ((- (th * <i> )) ExpSeq ) . n

proof

defpred S₁[ Element of NAT ] means (((th * <i> ) ExpSeq ) . $1) *' = ((- (th * <i> )) ExpSeq ) . $1;
(((th * <i> ) ExpSeq ) . 0 ) *' = 1r by Th4, COMPLEX1:115
.= ((- (th * <i> )) ExpSeq ) . 0 by Th4 ;
then A2: S₁[ 0 ] ;
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: (((th * <i> ) ExpSeq ) . n) *' = ((- (th * <i> )) ExpSeq ) . n ; :: thesis: S₁[n + 1]
thus (((th * <i> ) ExpSeq ) . (n + 1)) *' = (((((th * <i> ) ExpSeq ) . n) * (th * <i> )) / ((n + 1) + (0 * <i> ))) *' by Th4
.= ((((th * <i> ) ExpSeq ) . n) * ((th * <i> ) / ((n + 1) + (0 * <i> )))) *'
.= (((- (th * <i> )) ExpSeq ) . n) * (((th * <i> ) / (n + 1)) *' ) by A4, COMPLEX1:121
.= (((- (th * <i> )) ExpSeq ) . n) * (((0 + (th * <i> )) *' ) / ((n + 1) *' )) by COMPLEX1:123
.= (((- (th * <i> )) ExpSeq ) . n) * ((0 + ((- th) * <i> )) / (((n + 1) + (0 * <i> )) *' )) by Lm1
.= (((- (th * <i> )) ExpSeq ) . n) * ((0 + ((- th) * <i> )) / ((n + 1) + ((- 0 ) * <i> ))) by Lm1
.= ((((- (th * <i> )) ExpSeq ) . n) * (- (th * <i> ))) / ((n + 1) + (0 * <i> ))
.= ((- (th * <i> )) ExpSeq ) . (n + 1) by Th4 ; :: thesis: verum

end;

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

end;

defpred S₁[ Element of NAT ] means ((Partial_Sums ((th * <i> ) ExpSeq )) *' ) . $1 = (Partial_Sums ((- (th * <i> )) ExpSeq )) . $1;
((Partial_Sums ((th * <i> ) ExpSeq )) *' ) . 0 = ((Partial_Sums ((th * <i> ) ExpSeq )) . 0 ) *' by COMSEQ_2:def 2
.= (((th * <i> ) ExpSeq ) . 0 ) *' by COMSEQ_3:def 7
.= 1 by Th4, COMPLEX1:115
.= ((- (th * <i> )) ExpSeq ) . 0 by Th4
.= (Partial_Sums ((- (th * <i> )) ExpSeq )) . 0 by COMSEQ_3:def 7 ;
then A6: S₁[ 0 ] ;
A7: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: ((Partial_Sums ((th * <i> ) ExpSeq )) *' ) . n = (Partial_Sums ((- (th * <i> )) ExpSeq )) . n ; :: thesis: S₁[n + 1]
thus ((Partial_Sums ((th * <i> ) ExpSeq )) *' ) . (n + 1) = ((Partial_Sums ((th * <i> ) ExpSeq )) . (n + 1)) *' by COMSEQ_2:def 2
.= (((Partial_Sums ((th * <i> ) ExpSeq )) . n) + (((th * <i> ) ExpSeq ) . (n + 1))) *' by COMSEQ_3:def 7
.= (((Partial_Sums ((th * <i> ) ExpSeq )) . n) *' ) + ((((th * <i> ) ExpSeq ) . (n + 1)) *' ) by COMPLEX1:118
.= ((Partial_Sums ((- (th * <i> )) ExpSeq )) . n) + ((((th * <i> ) ExpSeq ) . (n + 1)) *' ) by A8, COMSEQ_2:def 2
.= ((Partial_Sums ((- (th * <i> )) ExpSeq )) . n) + (((- (th * <i> )) ExpSeq ) . (n + 1)) by A1
.= (Partial_Sums ((- (th * <i> )) ExpSeq )) . (n + 1) by COMSEQ_3:def 7 ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A7);
hence (Partial_Sums ((th * <i> ) ExpSeq )) *' = Partial_Sums ((- (th * <i> )) ExpSeq ) by FUNCT_2:113; :: thesis: verum

end;

hence (Sum ((th * <i> ) ExpSeq )) *' = Sum ((- (th * <i> )) ExpSeq ) by COMSEQ_2:12; :: thesis: verum