let X be Complex_Banach_Algebra; :: thesis: for k being Element of NAT
for z, w being Element of X st z,w are_commutative 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: for z, w being Element of X st z,w are_commutative 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 z, w be Element of X; :: thesis: ( z,w are_commutative implies (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums ((z + w) ExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k )
assume A1: z,w are_commutative ; :: thesis: (((Partial_Sums (z ExpSeq )) . k) * ((Partial_Sums (w ExpSeq )) . k)) - ((Partial_Sums ((z + w) ExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k
A2: (((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 A1, Th24
.= (((Partial_Sums (z ExpSeq )) * ((Partial_Sums (w ExpSeq )) . k)) . k) - ((Partial_Sums (Alfa k,z,w)) . k) by CLOPBAN3:def 9
.= ((Partial_Sums ((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k))) . k) - ((Partial_Sums (Alfa k,z,w)) . k) by Th9
.= ((Partial_Sums ((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k))) - (Partial_Sums (Alfa k,z,w))) . k by NORMSP_1:def 6
.= (Partial_Sums (((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k)) - (Alfa k,z,w))) . k by CLOPBAN3:20 ;
for l being Element of NAT st l <= k holds
(((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k)) - (Alfa k,z,w)) . l = (Conj k,z,w) . l

proof

let l be Element of NAT ; :: thesis: ( l <= k implies (((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k)) - (Alfa k,z,w)) . l = (Conj k,z,w) . l )
assume A3: l <= k ; :: thesis: (((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k)) - (Alfa k,z,w)) . l = (Conj k,z,w) . l
thus (((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k)) - (Alfa k,z,w)) . l = (((z ExpSeq ) * ((Partial_Sums (w ExpSeq )) . k)) . l) - ((Alfa k,z,w) . l) by NORMSP_1:def 6
.= (((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . k)) - ((Alfa k,z,w) . l) by CLOPBAN3:def 9
.= (((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . k)) - (((z ExpSeq ) . l) * ((Partial_Sums (w ExpSeq )) . (k -' l))) by A3, Def6
.= ((z ExpSeq ) . l) * (((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))) by CLOPBAN3:42
.= (Conj k,z,w) . l by A3, Def7 ; :: 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 A2, Th11; :: thesis: verum