let X be Complex_Banach_Algebra; :: thesis: for k being 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 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 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
then 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 Th24
.= (((Partial_Sums (z ExpSeq)) * ((Partial_Sums (w ExpSeq)) . k)) . k) - ((Partial_Sums (Alfa (k,z,w))) . k) by LOPBAN_3:def 6
.= ((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 3
.= (Partial_Sums (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) - (Alfa (k,z,w)))) . k by CLOPBAN3:16 ;
for l being 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 Nat; :: thesis: ( l <= k implies (((z ExpSeq) * ((Partial_Sums (w ExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l )
assume A2: 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 3
.= (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . k)) - ((Alfa (k,z,w)) . l) by LOPBAN_3:def 6
.= (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . k)) - (((z ExpSeq) . l) * ((Partial_Sums (w ExpSeq)) . (k -' l))) by A2, Def4
.= ((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))) by CLOPBAN3:38
.= (Conj (k,z,w)) . l by A2, Def5 ; :: 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, Th11; :: thesis: verum