let X be RealNormSpace; :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )
set RBLOP = R_Normed_Algebra_of_BoundedLinearOperators X;
set BS = R_NormSpace_of_BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set EXMULT = Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set NRM = BoundedLinearOperatorsNorm (X,X);
A1: ||.(0. (R_NormSpace_of_BoundedLinearOperators (X,X))).|| = (BoundedLinearOperatorsNorm (X,X)) . (0. (R_NormSpace_of_BoundedLinearOperators (X,X)))
.= ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| ;
thus ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| = 0 by A1; :: according to NORMSP_0:def 6 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )

A2: now :: thesis: for x, y being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a being Real holds
( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| )

let x, y be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: for a being Real holds
( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| )
let a be Real; :: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| )
reconsider x1 = x, y1 = y as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
A3: ||.x1.|| + ||.y1.|| = ((BoundedLinearOperatorsNorm (X,X)) . x1) + ||.y1.||
.= ((BoundedLinearOperatorsNorm (X,X)) . x1) + ((BoundedLinearOperatorsNorm (X,X)) . y1)
.= ||.x.|| + ( the normF of (R_Normed_Algebra_of_BoundedLinearOperators X) . y)
.= ||.x.|| + ||.y.|| ;
||.(x + y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (x,y))
.= ||.(x1 + y1).|| ;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A3, NORMSP_1:def 1; :: thesis: ( ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| )
A4: ||.x1.|| = (BoundedLinearOperatorsNorm (X,X)) . x1
.= ||.x.|| ;
0. (R_NormSpace_of_BoundedLinearOperators (X,X)) = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ;
hence ( ||.x.|| = 0 iff x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) by A4, NORMSP_0:def 5; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||
thus ||.(a * x).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,x))
.= ||.(a * x1).||
.= |.a.| * ||.x.|| by A4, NORMSP_1:def 1 ; :: thesis: verum

end;

A5: R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable

proof

let x be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
thus ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) by Th19; :: according to ALGSTR_0:def 11 :: thesis: verum

end;

( ( for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) ) & ( for a being Real
for v, w being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) ) by Th19;
hence ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) by A5, A2, NORMSP_1:def 1; :: thesis: verum