let z, w be Element of COMPLEX ; for n being Element of NAT holds (Partial_Sums ((z + w) ExpSeq )) . n = (Partial_Sums (Alfa n,z,w)) . n
let n be Element of NAT ; (Partial_Sums ((z + w) ExpSeq )) . n = (Partial_Sums (Alfa n,z,w)) . n
A1: (Partial_Sums ((z + w) ExpSeq )) . 0 =
((z + w) ExpSeq ) . 0
by COMSEQ_3:def 7
.=
1
by Th11
;
defpred S1[ Element of NAT ] means (Partial_Sums ((z + w) ExpSeq )) . $1 = (Partial_Sums (Alfa $1,z,w)) . $1;
A2:
0 -' 0 = 0
by XREAL_1:234;
A3: (Partial_Sums (Alfa 0 ,z,w)) . 0 =
(Alfa 0 ,z,w) . 0
by COMSEQ_3:def 7
.=
((z ExpSeq ) . 0 ) * ((Partial_Sums (w ExpSeq )) . 0 )
by A2, Def15
.=
((z ExpSeq ) . 0 ) * ((w ExpSeq ) . 0 )
by COMSEQ_3:def 7
.=
1r * ((w ExpSeq ) . 0 )
by Th11
.=
1
by Th11
;
A4:
S1[ 0 ]
by A1, A3;
A5:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A6:
(Partial_Sums ((z + w) ExpSeq )) . k = (Partial_Sums (Alfa k,z,w)) . k
;
S1[k + 1]
A7:
(Partial_Sums (Alfa (k + 1),z,w)) . (k + 1) =
((Partial_Sums (Alfa (k + 1),z,w)) . k) + ((Alfa (k + 1),z,w) . (k + 1))
by COMSEQ_3:def 7
.=
(((Partial_Sums (Alfa k,z,w)) . k) + ((Partial_Sums (Expan_e (k + 1),z,w)) . k)) + ((Alfa (k + 1),z,w) . (k + 1))
by Th13
.=
((Partial_Sums ((z + w) ExpSeq )) . k) + (((Partial_Sums (Expan_e (k + 1),z,w)) . k) + ((Alfa (k + 1),z,w) . (k + 1)))
by A6
;
A8:
(k + 1) -' (k + 1) = 0
by XREAL_1:234;
A9:
(Alfa (k + 1),z,w) . (k + 1) =
((z ExpSeq ) . (k + 1)) * ((Partial_Sums (w ExpSeq )) . 0 )
by A8, Def15
.=
((z ExpSeq ) . (k + 1)) * ((w ExpSeq ) . 0 )
by COMSEQ_3:def 7
.=
((z ExpSeq ) . (k + 1)) * 1
by Th11
.=
(Expan_e (k + 1),z,w) . (k + 1)
by Th14
;
A10:
((Partial_Sums (Expan_e (k + 1),z,w)) . k) + ((Alfa (k + 1),z,w) . (k + 1)) =
(Partial_Sums (Expan_e (k + 1),z,w)) . (k + 1)
by A9, COMSEQ_3:def 7
.=
((z + w) |^ (k + 1)) / ((k + 1) !c )
by Th9
;
A11:
(Partial_Sums (Alfa (k + 1),z,w)) . (k + 1) =
((Partial_Sums ((z + w) ExpSeq )) . k) + (((z + w) ExpSeq ) . (k + 1))
by A7, A10, Def8
.=
(Partial_Sums ((z + w) ExpSeq )) . (k + 1)
by COMSEQ_3:def 7
;
thus
(Partial_Sums ((z + w) ExpSeq )) . (k + 1) = (Partial_Sums (Alfa (k + 1),z,w)) . (k + 1)
by A11;
verum
end;
A12:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A4, A5);
thus
(Partial_Sums ((z + w) ExpSeq )) . n = (Partial_Sums (Alfa n,z,w)) . n
by A12; verum