let X be Banach_Algebra; :: thesis: 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; :: thesis: ( z,w are_commutative implies (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq) )
assume A1: z,w are_commutative ; :: thesis: (Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq)
deffunc H₁( 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 = H₁(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

proof

let k be Nat; :: thesis: seq . k = (Partial_Sums (Conj (k,z,w))) . k
k in NAT by ORDINAL1:def 12;
hence seq . k = (Partial_Sums (Conj (k,z,w))) . k by A2; :: thesis: verum

end;

now :: thesis: for k being Element of NAT holds seq . k = (((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) - (Partial_Sums ((z + w) rExpSeq))) . k

let k be Element of NAT ; :: thesis: seq . k = (((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) - (Partial_Sums ((z + w) rExpSeq))) . k
thus seq . k = (Partial_Sums (Conj (k,z,w))) . k by A2
.= (((Partial_Sums (z rExpSeq)) . k) * ((Partial_Sums (w rExpSeq)) . k)) - ((Partial_Sums ((z + w) rExpSeq)) . k) by A1, Th26
.= (((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) . k) - ((Partial_Sums ((z + w) rExpSeq)) . k) by LOPBAN_3:def 7
.= (((Partial_Sums (z rExpSeq)) * (Partial_Sums (w rExpSeq))) - (Partial_Sums ((z + w) rExpSeq))) . k by NORMSP_1:def 3 ; :: thesis: verum

end;

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; :: thesis: verum