begin
Lm1:
for X being Banach_Algebra
for z being Element of X
for n being Element of NAT holds
( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z )
Lm2:
for X being Banach_Algebra
for n being Element of NAT
for z, w being Element of X st z,w are_commutative holds
( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z )
Lm3:
for X being 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)