let X be 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 Th22
.= ((Alfa k,z,w) + (Expan_e (k + 1),z,w)) . l by NORMSP_1:def 5 ;
:: 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:20
.= ((Partial_Sums (Alfa k,z,w)) . k) + ((Partial_Sums (Expan_e (k + 1),z,w)) . k) by NORMSP_1:def 5 ;
:: thesis: verum