let X be ComplexNormSpace; :: thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexAlgebra-like & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexLinearSpace-like )
set C = C_Normed_Algebra_of_BoundedLinearOperators X;
set BS = C_NormSpace_of_BoundedLinearOperators X,X;
thus C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like :: thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexAlgebra-like & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexLinearSpace-like )

proof

let x, y be Point of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to CLVECT_1:def 11 :: thesis: for b₁ being Element of COMPLEX holds
( ( not ||.x.|| = 0 or x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) ) & ( not x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) or ||.x.|| = 0 ) & ||.(b₁ * x).|| = |.b₁.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Complex; :: thesis: ( ( not ||.x.|| = 0 or x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) ) & ( not x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) or ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider x1 = x, y1 = y as Point of (C_NormSpace_of_BoundedLinearOperators X,X) ;
A1: ||.x1.|| = ||.x.|| ;
0. (C_NormSpace_of_BoundedLinearOperators X,X) = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) ;
hence ( ||.x.|| = 0 iff x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) ) by A1, CLVECT_1:def 11; :: thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
thus ||.(a * x).|| = ||.(a * x1).||
.= |.a.| * ||.x.|| by A1, CLVECT_1:def 11 ; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
A2: ||.(x + y).|| = ||.(x1 + y1).|| ;
||.x1.|| + ||.y1.|| = ||.x.|| + ||.y.|| ;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A2, CLVECT_1:def 11; :: thesis: verum

end;

A3: C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable

proof

let x be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
thus x is right_complementable by Th19; :: thesis: verum

end;

A4: for x, y, z being Element of (C_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x ) by Th19;
set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
( ( for a being Complex
for v, w being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) & ( for a, b being Complex
for v being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds (a + b) * v = (a * v) + (b * v) ) & ( for a, b being Complex
for v being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds (a * b) * v = a * (b * v) ) & ( for v being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds 1r * v = v ) ) by Th19;
hence ( C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexAlgebra-like & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexLinearSpace-like ) by A3, A4, CFUNCDOM:def 9, CLVECT_1:def 2, GROUP_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, VECTSP_1:def 11, VECTSP_1:def 13; :: thesis: verum