let z, w be Element of COMPLEX ; :: thesis: 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 ; :: thesis: (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 SERIES_1:def 1
.= 1 by Th11 ;
defpred S₁[ 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;
(Partial_Sums (Alfa 0 ,z,w)) . 0 = (Alfa 0 ,z,w) . 0 by SERIES_1:def 1
.= ((z ExpSeq ) . 0 ) * ((Partial_Sums (w ExpSeq )) . 0 ) by A2, Def15
.= ((z ExpSeq ) . 0 ) * ((w ExpSeq ) . 0 ) by SERIES_1:def 1
.= 1r * ((w ExpSeq ) . 0 ) by Th11
.= 1 by Th11 ;
then A4: S₁[ 0 ] by A1;
A5: 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 A6: (Partial_Sums ((z + w) ExpSeq )) . k = (Partial_Sums (Alfa k,z,w)) . k ; :: thesis: S₁[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 SERIES_1:def 1
.= (((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 ;
(k + 1) -' (k + 1) = 0 by XREAL_1:234;
then (Alfa (k + 1),z,w) . (k + 1) = ((z ExpSeq ) . (k + 1)) * ((Partial_Sums (w ExpSeq )) . 0 ) by Def15
.= ((z ExpSeq ) . (k + 1)) * ((w ExpSeq ) . 0 ) by SERIES_1:def 1
.= ((z ExpSeq ) . (k + 1)) * 1 by Th11
.= (Expan_e (k + 1),z,w) . (k + 1) by Th14 ;
then ((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 SERIES_1:def 1
.= ((z + w) |^ (k + 1)) / ((k + 1) !c ) by Th9 ;
then (Partial_Sums (Alfa (k + 1),z,w)) . (k + 1) = ((Partial_Sums ((z + w) ExpSeq )) . k) + (((z + w) ExpSeq ) . (k + 1)) by A7, Def8
.= (Partial_Sums ((z + w) ExpSeq )) . (k + 1) by SERIES_1:def 1 ;
hence (Partial_Sums ((z + w) ExpSeq )) . (k + 1) = (Partial_Sums (Alfa (k + 1),z,w)) . (k + 1) ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A5);
hence (Partial_Sums ((z + w) ExpSeq )) . n = (Partial_Sums (Alfa n,z,w)) . n ; :: thesis: verum