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 9
.= ||.x.|| * ||.y.|| by CLOPBAN1:def 9 ;
||.(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 4
.= (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 8 :: 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 3 :: 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:8;

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:3
.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + ((- 1r) * (seq . m)))
.= ||.((seq . n) - (seq . m)).|| by CLVECT_1:3 ;
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:8;
then seq1 is convergent by CLOPBAN1:def 13;
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 15;
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:3
.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + ((- 1r) * g))
.= ||.((seq . n) - g).|| by CLVECT_1:3 ;
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 15; :: thesis: verum

end;

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