let X be Banach_Algebra; for z, w being Element of X st z,w are_commutative holds
(Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq)
let z, w be Element of X; ( z,w are_commutative implies (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq) )
assume A1:
z,w are_commutative
; (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq)
deffunc H1( Nat) -> Element of the carrier of X = (Partial_Sums (Conj ($1,z,w))) . $1;
ex seq being sequence of X st
for k being Element of NAT holds seq . k = H1(k)
from FUNCT_2:sch 4();
then consider seq being sequence of X such that
A2:
for k being Element of NAT holds seq . k = (Partial_Sums (Conj (k,z,w))) . k
;
A3:
for k being Nat holds seq . k = (Partial_Sums (Conj (k,z,w))) . k
then A4:
seq = ((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) - (Partial_Sums ((z + w) rExpSeq))
by FUNCT_2:63;
A5:
Partial_Sums (w rExpSeq) is convergent
by LOPBAN_3:def 1;
A6:
lim seq = 0. X
by A3, Th33;
A7:
Partial_Sums ((z + w) rExpSeq) is convergent
by LOPBAN_3:def 1;
A8:
Partial_Sums (z rExpSeq) is convergent
by LOPBAN_3:def 1;
then A9:
lim ((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) = (lim (Partial_Sums (z rExpSeq))) * (lim (Partial_Sums (w rExpSeq)))
by A5, Th8;
(Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq)) is convergent
by A8, A5, Th3;
hence
(Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq)
by A4, A7, A9, A6, Th1; verum