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 Nat holds (((th * <i>) ExpSeq) . n) *' = ((- (th * <i>)) ExpSeq) . n
proof
defpred S1[ Nat] means (((th * <i>) ExpSeq) . $1) *' = ((- (th * <i>)) ExpSeq) . $1;
(((th * <i>) ExpSeq) . 0) *' = 1r by Th3, COMPLEX1:30
.= ((- (th * <i>)) ExpSeq) . 0 by Th3 ;
then A2: S1[ 0 ] ;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: (((th * <i>) ExpSeq) . n) *' = ((- (th * <i>)) ExpSeq) . n ; :: thesis: S1[n + 1]
thus (((th * <i>) ExpSeq) . (n + 1)) *' = (((((th * <i>) ExpSeq) . n) * (th * <i>)) / ((n + 1) + (0 * <i>))) *' by Th3
.= ((((th * <i>) ExpSeq) . n) * ((th * <i>) / ((n + 1) + (0 * <i>)))) *'
.= (((- (th * <i>)) ExpSeq) . n) * (((th * <i>) / (n + 1)) *') by A4, COMPLEX1:35
.= (((- (th * <i>)) ExpSeq) . n) * (((0 + (th * <i>)) *') / ((n + 1) *')) by COMPLEX1:37
.= (((- (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 Th3 ; :: thesis: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A2, A3); :: thesis: verum
end;
defpred S1[ 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 SERIES_1:def 1
.= 1 by Th3, COMPLEX1:30
.= ((- (th * <i>)) ExpSeq) . 0 by Th3
.= (Partial_Sums ((- (th * <i>)) ExpSeq)) . 0 by SERIES_1:def 1 ;
then A5: S1[ 0 ] ;
A6: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: ((Partial_Sums ((th * <i>) ExpSeq)) *') . n = (Partial_Sums ((- (th * <i>)) ExpSeq)) . n ; :: thesis: S1[n + 1]
A8: n in NAT by ORDINAL1:def 12;
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 SERIES_1:def 1
.= (((Partial_Sums ((th * <i>) ExpSeq)) . n) *') + ((((th * <i>) ExpSeq) . (n + 1)) *') by COMPLEX1:32
.= ((Partial_Sums ((- (th * <i>)) ExpSeq)) . n) + ((((th * <i>) ExpSeq) . (n + 1)) *') by A7, COMSEQ_2:def 2, A8
.= ((Partial_Sums ((- (th * <i>)) ExpSeq)) . n) + (((- (th * <i>)) ExpSeq) . (n + 1)) by A1
.= (Partial_Sums ((- (th * <i>)) ExpSeq)) . (n + 1) by SERIES_1:def 1 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A5, A6);
 hence (Partial_Sums ((th * <i>) ExpSeq)) *' = Partial_Sums ((- (th * <i>)) ExpSeq) ; :: thesis: verum
end;
hence (Sum ((th * <i>) ExpSeq)) *' = Sum ((- (th * <i>)) ExpSeq) by COMSEQ_2:12; :: thesis: verum