let X be RealNormSpace; :: thesis: Ring_of_BoundedLinearOperators X is Ring
set R = Ring_of_BoundedLinearOperators X;
A1: Ring_of_BoundedLinearOperators X is right_complementable
proof
let x be Element of (Ring_of_BoundedLinearOperators X); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
thus ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) by Th13; :: according to ALGSTR_0:def 11 :: thesis: verum
end;
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 & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (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) ) by Th13;
hence Ring_of_BoundedLinearOperators X is Ring by A1, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 6, VECTSP_1:def 7; :: thesis: verum