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

let l be Element of 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 Th21
.= ((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 CLOPBAN3:15
.= ((Partial_Sums (Alfa (k,z,w))) . k) + ((Partial_Sums (Expan_e ((k + 1),z,w))) . k) by NORMSP_1:def 2 ;
:: thesis: verum