theorem Th13: :: CLOPBAN2:13

for X being ComplexNormSpace
for x, y, z being Element of (Ring_of_BoundedLinearOperators X) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )