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

proof

let x, y be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to LOPBAN_2: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 LOPBAN_1:def 11
.= ((BoundedLinearOperatorsNorm (X,X)) . x1) * ((BoundedLinearOperatorsNorm (X,X)) . y1) by LOPBAN_1:def 11
.= ||.x.|| * ((BoundedLinearOperatorsNorm (X,X)) . y)
.= ||.x.|| * ||.y.|| ;
||.(x * y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((FuncMult X) . (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. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| = (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X)
.= 1 by Th18 ;
hence R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 ; :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )
thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )

proof

let a be Real; :: according to LOPBAN_2:def 11 :: thesis: for x, y being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (x * y) = x * (a * y)
let x, y be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: a * (x * y) = x * (a * y)
thus a * (x * y) = (1 * a) * (x * y)
.= (1 * x) * (a * y) by Th19
.= x * (a * y) by Th19 ; :: thesis: verum

end;

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

proof

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

end;

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

proof

let x, y, z be Element of (R_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)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4
.= (y * x) + (z * x) by Def4 ; :: thesis: verum

end;

now :: thesis: for seq being sequence of (R_Normed_Algebra_of_BoundedLinearOperators X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent

let seq be sequence of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume A2: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent
reconsider seq1 = seq as sequence of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;

now :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r

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

now :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r

let n, m be 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)) . ((seq1 . n) + (- (seq1 . m)))
.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * (seq1 . m)))) by RLVECT_1:16
.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * (seq . m))))
.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- (seq . m))) by RLVECT_1:16
.= ||.((seq . n) - (seq . m)).|| ;
hence ||.((seq1 . n) - (seq1 . m)).|| < r by A3, A4; :: thesis: verum

end;

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

end;

then seq1 is Cauchy_sequence_by_Norm by RSSPACE3:8;
then seq1 is convergent by LOPBAN_1:def 15;
then consider g1 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) such that
A5: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq1 . n) - g1).|| < r by NORMSP_1:def 6;
reconsider g = g1 as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;

now :: thesis: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - g).|| < r

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

now :: thesis: for n being Nat st m <= n holds
||.((seq . n) - g).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - g).|| < r )
assume A7: m <= n ; :: thesis: ||.((seq . n) - g).|| < r
||.((seq1 . n) - g1).|| = (BoundedLinearOperatorsNorm (X,X)) . ((seq1 . n) + (- g1))
.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * g1))) by RLVECT_1:16
.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * g)))
.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- g)) by RLVECT_1:16
.= ||.((seq . n) - g).|| ;
hence ||.((seq . n) - g).|| < r by A6, A7; :: thesis: verum

end;

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

end;

hence seq is convergent by NORMSP_1:def 6; :: thesis: verum

end;

hence R_Normed_Algebra_of_BoundedLinearOperators X is complete ; :: thesis: verum