let X be Banach_Algebra; :: thesis: for w, z being Element of X
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 w, z be Element of X; :: 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)

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 )
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 Th22
.= ((Alfa (k,z,w)) + (Expan_e ((k + 1),z,w))) . l by NORMSP_1:def 2 ;
:: 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 Th11
.= ((Partial_Sums (Alfa (k,z,w))) + (Partial_Sums (Expan_e ((k + 1),z,w)))) . k by LOPBAN_3:15
.= ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) by NORMSP_1:def 2 ;
:: thesis: verum