let z, w be Element of COMPLEX ; :: 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)

A1: 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 A2: l <= k ; :: thesis: (Alfa (k + 1),z,w) . l = ((Alfa k,z,w) + (Expan_e (k + 1),z,w)) . l
thus (Alfa (k + 1),z,w) . l = ((Alfa k,z,w) . l) + ((Expan_e (k + 1),z,w) . l) by A2, Th12
.= ((Alfa k,z,w) + (Expan_e (k + 1),z,w)) . l by VALUED_1:1 ; :: thesis: verum

end;

thus (Partial_Sums (Alfa (k + 1),z,w)) . k = (Partial_Sums ((Alfa k,z,w) + (Expan_e (k + 1),z,w))) . k by A1, 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 ; :: thesis: verum