let w, z be Complex; :: thesis: for k being Nat holds (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)
let k be Nat; :: thesis: (Partial_Sums (Alfa ((k + 1),z,w))) . k = ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k)
A1: k in NAT by ORDINAL1:def 12;

now :: thesis: for l being Nat st l <= k holds
(Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l

let l be Nat; :: thesis: ( l <= k implies (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l )
A2: l in NAT by ORDINAL1:def 12;
assume l <= k ; :: thesis: (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l
hence (Alfa ((k + 1),z,w)) . l = ((Alfa (k,z,w)) . l) + ((Expan_e ((k + 1),z,w)) . l) by Th11
.= ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l by VALUED_1:1, A2 ;
:: thesis: verum

end;

hence (Partial_Sums (Alfa ((k + 1),z,w))) . k = (Partial_Sums ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w)))) . k by COMSEQ_3:35
.= ((Partial_Sums (Alfa (k,z,w))) + (Partial_Sums (Expan_e ((k + 1),z,w)))) . k by COMSEQ_3:27
.= ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) by VALUED_1:1, A1 ;
:: thesis: verum