let X be Banach_Algebra; for k being 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 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 z, w be Element of X; ( 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
; (((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 6
.=
((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 3
.=
(Partial_Sums (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) - (Alfa (k,z,w)))) . k
by LOPBAN_3:16
;
for l being 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
Nat;
( l <= k implies (((z rExpSeq) * ((Partial_Sums (w rExpSeq)) . k)) - (Alfa (k,z,w))) . l = (Conj (k,z,w)) . l )
assume A2:
l <= k
;
(((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 3
.=
(((z rExpSeq) . l) * ((Partial_Sums (w rExpSeq)) . k)) - ((Alfa (k,z,w)) . l)
by LOPBAN_3:def 6
.=
(((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:38
.=
(Conj (k,z,w)) . l
by A2, Def9
;
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; verum