set NRM = BoundedLinearOperatorsNorm X,X;
set UNIT = FuncUnit X;
set MULT = FuncMult X;
set ADD = Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X);
set BS = C_NormSpace_of_BoundedLinearOperators X,X;
set BLOP = BoundedLinearOperators X,X;
set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
thus C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_1 :: according to CLOPBAN2:def 12 :: thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 & C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )

proof

let x, y be Point of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to CLOPBAN2:def 9 :: thesis: ||.(x * y).|| <= ||.x.|| * ||.y.||
reconsider x1 = x, y1 = y as Element of BoundedLinearOperators X,X ;
A1: ((BoundedLinearOperatorsNorm X,X) . (modetrans x1,X,X)) * ((BoundedLinearOperatorsNorm X,X) . (modetrans y1,X,X)) = ((BoundedLinearOperatorsNorm X,X) . x1) * ((BoundedLinearOperatorsNorm X,X) . (modetrans y1,X,X)) by CLOPBAN1:def 10
.= ||.x.|| * ||.y.|| by CLOPBAN1:def 10 ;
||.(x * y).|| = (BoundedLinearOperatorsNorm X,X) . (x1 * y1) by Def4
.= (BoundedLinearOperatorsNorm X,X) . ((modetrans x1,X,X) * (modetrans y1,X,X)) ;
hence ||.(x * y).|| <= ||.x.|| * ||.y.|| by A1, Th2; :: thesis: verum

end;

||.(1. (C_Normed_Algebra_of_BoundedLinearOperators X)).|| = 1 by Th18;
hence C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 by Def10; :: thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
thus C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 :: thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )

proof

let a be Complex; :: according to CLOPBAN2:def 11 :: thesis: for x, y being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) holds a * (x * y) = x * (a * y)
let x, y be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: a * (x * y) = x * (a * y)
thus a * (x * y) = (1r * a) * (x * y) by COMPLEX1:def 7
.= (1r * x) * (a * y) by Th19
.= x * (a * y) by Th19 ; :: thesis: verum

end;

thus C_Normed_Algebra_of_BoundedLinearOperators X is left_unital :: thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )

proof

let x be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def 19 :: thesis: (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) * x = x
reconsider xx = x as Element of BoundedLinearOperators X,X ;
thus (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; :: thesis: verum

end;

thus C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive :: thesis: C_Normed_Algebra_of_BoundedLinearOperators X is complete

proof

let x, y, z be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def 12 :: thesis: (y + z) * x = (y * x) + (z * x)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators X,X ;
thus (y + z) * x = (yy + zz) * xx by Def4
.= (yy * xx) + (zz * xx) by Th10
.= (Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . (yy * xx),((FuncMult X) . zz,xx) by Def4
.= (y * x) + (z * x) by Def4 ; :: thesis: verum

end;

now

let seq be sequence of (C_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: ( seq is CCauchy implies seq is convergent )
assume A2: seq is CCauchy ; :: thesis: seq is convergent
reconsider seq1 = seq as sequence of (C_NormSpace_of_BoundedLinearOperators X,X) ;

now

let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r
then consider k being Element of NAT such that
A3: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A2, CSSPACE3:10;

now

let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies ||.((seq1 . n) - (seq1 . m)).|| < r )
assume A4: ( n >= k & m >= k ) ; :: thesis: ||.((seq1 . n) - (seq1 . m)).|| < r
||.((seq1 . n) - (seq1 . m)).|| = (BoundedLinearOperatorsNorm X,X) . ((Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . (seq1 . n),((- 1r ) * (seq1 . m))) by CLVECT_1:4
.= (BoundedLinearOperatorsNorm X,X) . ((seq . n) + ((- 1r ) * (seq . m)))
.= ||.((seq . n) - (seq . m)).|| by CLVECT_1:4 ;
hence ||.((seq1 . n) - (seq1 . m)).|| < r by A3, A4; :: thesis: verum

end;

hence ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r ; :: thesis: verum

end;

then seq1 is CCauchy by CSSPACE3:10;
then seq1 is convergent by CLOPBAN1:def 14;
then consider g1 being Point of (C_NormSpace_of_BoundedLinearOperators X,X) such that
A5: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq1 . n) - g1).|| < r by CLVECT_1:def 16;
reconsider g = g1 as Point of (C_Normed_Algebra_of_BoundedLinearOperators X) ;

now

let r be Real; :: thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - g).|| < r )
assume 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - g).|| < r
then consider m being Element of NAT such that
A6: for n being Element of NAT st m <= n holds
||.((seq1 . n) - g1).|| < r by A5;

now

let n be Element of NAT ; :: thesis: ( m <= n implies ||.((seq . n) - g).|| < r )
assume A7: m <= n ; :: thesis: ||.((seq . n) - g).|| < r
||.((seq1 . n) - g1).|| = (BoundedLinearOperatorsNorm X,X) . ((Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . (seq1 . n),((- 1r ) * g1)) by CLVECT_1:4
.= (BoundedLinearOperatorsNorm X,X) . ((seq . n) + ((- 1r ) * g))
.= ||.((seq . n) - g).|| by CLVECT_1:4 ;
hence ||.((seq . n) - g).|| < r by A6, A7; :: thesis: verum

end;

hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - g).|| < r ; :: thesis: verum

end;

hence seq is convergent by CLVECT_1:def 16; :: thesis: verum

end;

hence C_Normed_Algebra_of_BoundedLinearOperators X is complete by CLOPBAN1:def 14; :: thesis: verum