let z, w be Element of COMPLEX ; :: thesis: for k being Element of NAT holds (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums ((z + w) ExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k
let k be Element of NAT ; :: thesis: (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums ((z + w) ExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k
A1: (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums ((z + w) ExpSeq )) . k) = (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums (Alfa k,z,w)) . k) by Th15
.= ((((Partial_Sums (w ExpSeq )) . k) (#) (Partial_Sums (z ExpSeq ))) . k) - ((Partial_Sums (Alfa k,z,w)) . k) by VALUED_1:6
.= ((Partial_Sums (((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq ))) . k) - ((Partial_Sums (Alfa k,z,w)) . k) by COMSEQ_3:29
.= ((Partial_Sums (((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq ))) . k) + ((- (Partial_Sums (Alfa k,z,w))) . k) by VALUED_1:8
.= ((Partial_Sums (((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq ))) - (Partial_Sums (Alfa k,z,w))) . k by VALUED_1:1
.= (Partial_Sums ((((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - (Alfa k,z,w))) . k by COMSEQ_3:28 ;
for l being Element of NAT st l <= k holds
((((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - (Alfa k,z,w)) . l = (Conj k,z,w) . l

proof

let l be Element of NAT ; :: thesis: ( l <= k implies ((((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - (Alfa k,z,w)) . l = (Conj k,z,w) . l )
assume A3: l <= k ; :: thesis: ((((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - (Alfa k,z,w)) . l = (Conj k,z,w) . l
thus ((((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) - (Alfa k,z,w)) . l = ((((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) . l) + ((- (Alfa k,z,w)) . l) by VALUED_1:1
.= ((((Partial_Sums (w ExpSeq )) . k) (#) (z ExpSeq )) . l) - ((Alfa k,z,w) . l) by VALUED_1:8
.= (((Partial_Sums (w ExpSeq )) . k) * ((z ExpSeq ) . l)) - ((Alfa k,z,w) . l) by VALUED_1:6
.= (((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . k)) - (((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . (k -' l))) by A3, Def15
.= ((z ExpSeq ) . l) * (((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l)))
.= (Conj k,z,w) . l by A3, Def17 ; :: thesis: verum

end;

hence (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums ((z + w) ExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k by A1, COMSEQ_3:35; :: thesis: verum