theorem Th38: :: CLOPBAN3:38

for X being Complex_Banach_Algebra
for x, y, z being Element of X
for a, b being Complex holds
( a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 )