let X be 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 rExpSeq )) . k) * ((Partial_Sums (w rExpSeq )) . k)) - ((Partial_Sums ((z + w) rExpSeq )) . 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 rExpSeq )) . k) * ((Partial_Sums (w rExpSeq )) . k)) - ((Partial_Sums ((z + w) rExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k
let z, w be Element of X; :: thesis: ( z,w are_commutative implies (((Partial_Sums (z rExpSeq )) . k) * ((Partial_Sums (w rExpSeq )) . k)) - ((Partial_Sums ((z + w) rExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k )
assume z,w are_commutative ; :: thesis: (((Partial_Sums (z rExpSeq )) . k) * ((Partial_Sums (w rExpSeq )) . k)) - ((Partial_Sums ((z + w) rExpSeq )) . k) = (Partial_Sums (Conj k,z,w)) . k
then A1: (((Partial_Sums (z rExpSeq )) . k) * ((Partial_Sums (w rExpSeq )) . k)) - ((Partial_Sums ((z + w) rExpSeq )) . k) = (((Partial_Sums (z rExpSeq )) . k) * ((Partial_Sums (w rExpSeq )) . k)) - ((Partial_Sums (Alfa k,z,w)) . k) by Th25
.= (((Partial_Sums (z rExpSeq )) * ((Partial_Sums (w rExpSeq )) . k)) . k) - ((Partial_Sums (Alfa k,z,w)) . k) by LOPBAN_3:def 10
.= ((Partial_Sums ((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k))) . k) - ((Partial_Sums (Alfa k,z,w)) . k) by Th9
.= ((Partial_Sums ((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k))) - (Partial_Sums (Alfa k,z,w))) . k by NORMSP_1:def 6
.= (Partial_Sums (((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k)) - (Alfa k,z,w))) . k by LOPBAN_3:21 ;
for l being Element of NAT st l <= k holds
(((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k)) - (Alfa k,z,w)) . l = (Conj k,z,w) . l

proof

let l be Element of NAT ; :: thesis: ( l <= k implies (((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k)) - (Alfa k,z,w)) . l = (Conj k,z,w) . l )
assume A2: l <= k ; :: thesis: (((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k)) - (Alfa k,z,w)) . l = (Conj k,z,w) . l
thus (((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k)) - (Alfa k,z,w)) . l = (((z rExpSeq ) * ((Partial_Sums (w rExpSeq )) . k)) . l) - ((Alfa k,z,w) . l) by NORMSP_1:def 6
.= (((z rExpSeq ) . l) * ((Partial_Sums (w rExpSeq )) . k)) - ((Alfa k,z,w) . l) by LOPBAN_3:def 10
.= (((z rExpSeq ) . l) * ((Partial_Sums (w rExpSeq )) . k)) - (((z rExpSeq ) . l) * ((Partial_Sums (w rExpSeq )) . (k -' l))) by A2, Def8
.= ((z rExpSeq ) . l) * (((Partial_Sums (w rExpSeq )) . k) - ((Partial_Sums (w rExpSeq )) . (k -' l))) by LOPBAN_3:43
.= (Conj k,z,w) . l by A2, Def9 ; :: thesis: verum

end;

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