:: LOPBAN_2 semantic presentation

begin

theorem Th1: :: LOPBAN_2:1
for X, Y, Z being RealLinearSpace
for f being LinearOperator of X,Y
for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
proof
let X, Y, Z be RealLinearSpace; ::_thesis: for f being LinearOperator of X,Y
for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
let f be LinearOperator of X,Y; ::_thesis: for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
let g be LinearOperator of Y,Z; ::_thesis: g * f is LinearOperator of X,Z
A1: now__::_thesis:_for_v_being_VECTOR_of_X
for_a_being_Real_holds_(g_*_f)_._(a_*_v)_=_a_*_((g_*_f)_._v)
let v be VECTOR of X; ::_thesis: for a being Real holds (g * f) . (a * v) = a * ((g * f) . v)
let a be Real; ::_thesis: (g * f) . (a * v) = a * ((g * f) . v)
thus (g * f) . (a * v) = g . (f . (a * v)) by FUNCT_2:15
.= g . (a * (f . v)) by LOPBAN_1:def_5
.= a * (g . (f . v)) by LOPBAN_1:def_5
.= a * ((g * f) . v) by FUNCT_2:15 ; ::_thesis: verum
end;
now__::_thesis:_for_v,_w_being_VECTOR_of_X_holds_(g_*_f)_._(v_+_w)_=_((g_*_f)_._v)_+_((g_*_f)_._w)
let v, w be VECTOR of X; ::_thesis: (g * f) . (v + w) = ((g * f) . v) + ((g * f) . w)
thus (g * f) . (v + w) = g . (f . (v + w)) by FUNCT_2:15
.= g . ((f . v) + (f . w)) by VECTSP_1:def_20
.= (g . (f . v)) + (g . (f . w)) by VECTSP_1:def_20
.= ((g * f) . v) + (g . (f . w)) by FUNCT_2:15
.= ((g * f) . v) + ((g * f) . w) by FUNCT_2:15 ; ::_thesis: verum
end;
hence  g * f is LinearOperator of X,Z by A1, VECTSP_1:def_20, LOPBAN_1:def_5; ::_thesis: verum
end;

theorem Th2: :: LOPBAN_2:2
for X, Y, Z being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y
for g being Lipschitzian LinearOperator of Y,Z holds
( g * f is Lipschitzian LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) )
proof
let X, Y, Z be RealNormSpace; ::_thesis: for f being Lipschitzian LinearOperator of X,Y
for g being Lipschitzian LinearOperator of Y,Z holds
( g * f is Lipschitzian LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) )
let f be Lipschitzian LinearOperator of X,Y; ::_thesis: for g being Lipschitzian LinearOperator of Y,Z holds
( g * f is Lipschitzian LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) )
let g be Lipschitzian LinearOperator of Y,Z; ::_thesis: ( g * f is Lipschitzian LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) )
reconsider ff = f as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def_9;
reconsider gg = g as Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def_9;
A1: now__::_thesis:_for_v_being_VECTOR_of_X_holds_||.((g_*_f)_._v).||_<=_(||.gg.||_*_||.ff.||)_*_||.v.||
let v be VECTOR of X; ::_thesis: ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.||
 0 <= ||.gg.|| by NORMSP_1:4;
then A2: ||.gg.|| * ||.(f . v).|| <= ||.gg.|| * (||.ff.|| * ||.v.||) by LOPBAN_1:32, XREAL_1:64;
 ( ||.((g * f) . v).|| = ||.(g . (f . v)).|| & ||.(g . (f . v)).|| <= ||.gg.|| * ||.(f . v).|| ) by FUNCT_2:15, LOPBAN_1:32;
hence  ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.|| by A2, XXREAL_0:2; ::_thesis: verum
end;
A3: ( 0 <= ||.gg.|| & 0 <= ||.ff.|| ) by NORMSP_1:4;
then reconsider gf = g * f as Lipschitzian LinearOperator of X,Z by A1, Th1, LOPBAN_1:def_8;
set K = ||.gg.|| * ||.ff.||;
A4: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.((g_*_f)_._t).||_<=_||.gg.||_*_||.ff.||
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.|| )
assume  ||.t.|| <= 1 ; ::_thesis: ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.||
then A5: (||.gg.|| * ||.ff.||) * ||.t.|| <= (||.gg.|| * ||.ff.||) * 1 by A3, XREAL_1:64;
 ||.((g * f) . t).|| <= (||.gg.|| * ||.ff.||) * ||.t.|| by A1;
hence  ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.|| by A5, XXREAL_0:2; ::_thesis: verum
end;
A6: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_gf_holds_
r_<=_||.gg.||_*_||.ff.||
let r be Real; ::_thesis: ( r in PreNorms gf implies r <= ||.gg.|| * ||.ff.|| )
assume  r in PreNorms gf ; ::_thesis: r <= ||.gg.|| * ||.ff.||
then  ex t being VECTOR of X st
( r = ||.(gf . t).|| & ||.t.|| <= 1 ) ;
hence  r <= ||.gg.|| * ||.ff.|| by A4; ::_thesis: verum
end;
 ( ( for s being real number st s in PreNorms gf holds
s <= ||.gg.|| * ||.ff.|| ) implies upper_bound (PreNorms gf) <= ||.gg.|| * ||.ff.|| ) by SEQ_4:45;
hence  ( g * f is Lipschitzian LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) ) by A1, A6, LOPBAN_1:30; ::_thesis: verum
end;

definition
let X be RealNormSpace;
let f, g be Lipschitzian LinearOperator of X,X;
:: original: *
redefine funcg * f ->  Lipschitzian LinearOperator of X,X;
correctness
coherence
g * f is Lipschitzian LinearOperator of X,X;
by Th2;
end;

definition
let X be RealNormSpace;
let f, g be Element of BoundedLinearOperators (X,X);
funcf + g ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 1
(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g);
correctness
coherence
(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g) is Element of BoundedLinearOperators (X,X);
;
end;

:: deftheorem  defines + LOPBAN_2:def_1_:_
 for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X) holds f + g = (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g);

definition
let X be RealNormSpace;
let f, g be Element of BoundedLinearOperators (X,X);
funcg * f ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 2
(modetrans (g,X,X)) * (modetrans (f,X,X));
correctness
coherence
(modetrans (g,X,X)) * (modetrans (f,X,X)) is Element of BoundedLinearOperators (X,X);
by LOPBAN_1:def_9;
end;

:: deftheorem  defines * LOPBAN_2:def_2_:_
 for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X) holds g * f = (modetrans (g,X,X)) * (modetrans (f,X,X));

definition
let X be RealNormSpace;
let f be Element of BoundedLinearOperators (X,X);
let a be Real;
funca * f ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 3
(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f);
correctness
coherence
(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f) is Element of BoundedLinearOperators (X,X);
;
end;

:: deftheorem  defines * LOPBAN_2:def_3_:_
 for X being RealNormSpace
for f being Element of BoundedLinearOperators (X,X)
for a being Real holds a * f = (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f);

definition
let X be RealNormSpace;
func FuncMult X ->  BinOp of (BoundedLinearOperators (X,X)) means :Def4: :: LOPBAN_2:def 4
 for f, g being Element of BoundedLinearOperators (X,X) holds it . (f,g) = f * g;
existence
 ex b1 being BinOp of (BoundedLinearOperators (X,X)) st
for f, g being Element of BoundedLinearOperators (X,X) holds b1 . (f,g) = f * g
proof
deffunc H1( Element of BoundedLinearOperators (X,X), Element of BoundedLinearOperators (X,X)) ->  Element of BoundedLinearOperators (X,X) = $1 * $2;
consider F being BinOp of (BoundedLinearOperators (X,X)) such that
A1: for x, y being Element of BoundedLinearOperators (X,X) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  F ; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X) holds F . (f,g) = f * g
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: F . (f,g) = f * g
thus  F . (f,g) = f * g by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (BoundedLinearOperators (X,X)) st ( for f, g being Element of BoundedLinearOperators (X,X) holds b1 . (f,g) = f * g ) & ( for f, g being Element of BoundedLinearOperators (X,X) holds b2 . (f,g) = f * g ) holds
b1 = b2
proof
let it1, it2 be BinOp of (BoundedLinearOperators (X,X)); ::_thesis: ( ( for f, g being Element of BoundedLinearOperators (X,X) holds it1 . (f,g) = f * g ) & ( for f, g being Element of BoundedLinearOperators (X,X) holds it2 . (f,g) = f * g ) implies it1 = it2 )
assume that
A2: for f, g being Element of BoundedLinearOperators (X,X) holds it1 . (f,g) = f * g and
A3: for f, g being Element of BoundedLinearOperators (X,X) holds it2 . (f,g) = f * g ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_BoundedLinearOperators_(X,X)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = f * g by A2
.= it2 . (f,g) by A3 ; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines FuncMult LOPBAN_2:def_4_:_
 for X being RealNormSpace
for b2 being BinOp of (BoundedLinearOperators (X,X)) holds
( b2 = FuncMult X iff for f, g being Element of BoundedLinearOperators (X,X) holds b2 . (f,g) = f * g );

theorem Th3: :: LOPBAN_2:3
for X being RealNormSpace holds id the carrier of X is Lipschitzian LinearOperator of X,X
proof
let X be RealNormSpace; ::_thesis: id the carrier of X is Lipschitzian LinearOperator of X,X
A1: now__::_thesis:_for_v,_w_being_VECTOR_of_X_holds_(id_the_carrier_of_X)_._(v_+_w)_=_((id_the_carrier_of_X)_._v)_+_((id_the_carrier_of_X)_._w)
let v, w be VECTOR of X; ::_thesis: (id the carrier of X) . (v + w) = ((id the carrier of X) . v) + ((id the carrier of X) . w)
thus (id the carrier of X) . (v + w) = v + w by FUNCT_1:18
.= ((id the carrier of X) . v) + w by FUNCT_1:18
.= ((id the carrier of X) . v) + ((id the carrier of X) . w) by FUNCT_1:18 ; ::_thesis: verum
end;
A2: now__::_thesis:_for_v_being_VECTOR_of_X
for_a_being_Real_holds_(id_the_carrier_of_X)_._(a_*_v)_=_a_*_((id_the_carrier_of_X)_._v)
let v be VECTOR of X; ::_thesis: for a being Real holds (id the carrier of X) . (a * v) = a * ((id the carrier of X) . v)
let a be Real; ::_thesis: (id the carrier of X) . (a * v) = a * ((id the carrier of X) . v)
thus (id the carrier of X) . (a * v) = a * v by FUNCT_1:18
.= a * ((id the carrier of X) . v) by FUNCT_1:18 ; ::_thesis: verum
end;
 for v being VECTOR of X holds ||.((id the carrier of X) . v).|| <= 1 * ||.v.|| by FUNCT_1:18;
hence  id the carrier of X is Lipschitzian LinearOperator of X,X by A1, A2, VECTSP_1:def_20, LOPBAN_1:def_5, LOPBAN_1:def_8; ::_thesis: verum
end;

definition
let X be RealNormSpace;
func FuncUnit X ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 5
 id the carrier of X;
coherence
 id the carrier of X is Element of BoundedLinearOperators (X,X)
proof
 id the carrier of X is Lipschitzian LinearOperator of X,X by Th3;
hence  id the carrier of X is Element of BoundedLinearOperators (X,X) by LOPBAN_1:def_9; ::_thesis: verum
end;
end;

:: deftheorem  defines FuncUnit LOPBAN_2:def_5_:_
 for X being RealNormSpace holds FuncUnit X = id the carrier of X;

theorem Th4: :: LOPBAN_2:4
for X being RealNormSpace
for f, g, h being Lipschitzian LinearOperator of X,X holds
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
proof
let X be RealNormSpace; ::_thesis: for f, g, h being Lipschitzian LinearOperator of X,X holds
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
let f, g, h be Lipschitzian LinearOperator of X,X; ::_thesis: ( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
now__::_thesis:_(_(_for_x_being_VECTOR_of_X_holds_h_._x_=_f_._(g_._x)_)_implies_h_=_f_*_g_)
assume A1: for x being VECTOR of X holds h . x = f . (g . x) ; ::_thesis: h = f * g
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(f_*_g)_._x_=_h_._x
let x be VECTOR of X; ::_thesis: (f * g) . x = h . x
thus (f * g) . x = f . (g . x) by FUNCT_2:15
.= h . x by A1 ; ::_thesis: verum
end;
hence  h = f * g by FUNCT_2:63; ::_thesis: verum
end;
hence  ( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) ) by FUNCT_2:15; ::_thesis: verum
end;

theorem Th5: :: LOPBAN_2:5
for X being RealNormSpace
for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h
proof
let X be RealNormSpace; ::_thesis: for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h
let f, g, h be Lipschitzian LinearOperator of X,X; ::_thesis: f * (g * h) = (f * g) * h
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(f_*_(g_*_h))_._x_=_((f_*_g)_*_h)_._x
let x be VECTOR of X; ::_thesis: (f * (g * h)) . x = ((f * g) * h) . x
thus (f * (g * h)) . x = f . ((g * h) . x) by Th4
.= f . (g . (h . x)) by Th4
.= (f * g) . (h . x) by FUNCT_2:15
.= ((f * g) * h) . x by Th4 ; ::_thesis: verum
end;
hence  f * (g * h) = (f * g) * h by FUNCT_2:63; ::_thesis: verum
end;

theorem Th6: :: LOPBAN_2:6
for X being RealNormSpace
for f being Lipschitzian LinearOperator of X,X holds
( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
proof
let X be RealNormSpace; ::_thesis: for f being Lipschitzian LinearOperator of X,X holds
( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
reconsider ii = id the carrier of X as Lipschitzian LinearOperator of X,X by Th3;
let f be Lipschitzian LinearOperator of X,X; ::_thesis: ( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
A1: now__::_thesis:_for_x_being_VECTOR_of_X_holds_((id_the_carrier_of_X)_*_f)_._x_=_f_._x
let x be VECTOR of X; ::_thesis: ((id the carrier of X) * f) . x = f . x
thus ((id the carrier of X) * f) . x = (ii * f) . x
.= ii . (f . x) by Th4
.= f . x by FUNCT_1:18 ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(f_*_(id_the_carrier_of_X))_._x_=_f_._x
let x be VECTOR of X; ::_thesis: (f * (id the carrier of X)) . x = f . x
thus (f * (id the carrier of X)) . x = (f * ii) . x
.= f . (ii . x) by Th4
.= f . x by FUNCT_1:18 ; ::_thesis: verum
end;
hence  ( f * (id the carrier of X) = f & (id the carrier of X) * f = f ) by A1, FUNCT_2:63; ::_thesis: verum
end;

theorem Th7: :: LOPBAN_2:7
for X being RealNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h
proof
let X be RealNormSpace; ::_thesis: for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h
let f, g, h be Element of BoundedLinearOperators (X,X); ::_thesis: f * (g * h) = (f * g) * h
 modetrans ((g * h),X,X) = (modetrans (g,X,X)) * (modetrans (h,X,X)) by LOPBAN_1:def_11;
then  (modetrans (f,X,X)) * (modetrans ((g * h),X,X)) = ((modetrans (f,X,X)) * (modetrans (g,X,X))) * (modetrans (h,X,X)) by Th5;
hence  f * (g * h) = (f * g) * h by LOPBAN_1:def_11; ::_thesis: verum
end;

theorem Th8: :: LOPBAN_2:8
for X being RealNormSpace
for f being Element of BoundedLinearOperators (X,X) holds
( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
proof
let X be RealNormSpace; ::_thesis: for f being Element of BoundedLinearOperators (X,X) holds
( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
let f be Element of BoundedLinearOperators (X,X); ::_thesis: ( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
 id the carrier of X is Lipschitzian LinearOperator of X,X by Th3;
then  id the carrier of X is Element of BoundedLinearOperators (X,X) by LOPBAN_1:def_9;
then A1: modetrans ((id the carrier of X),X,X) = id the carrier of X by LOPBAN_1:def_11;
hence f * (FuncUnit X) = modetrans (f,X,X) by Th6
.= f by LOPBAN_1:def_11 ;
::_thesis: (FuncUnit X) * f = f
thus (FuncUnit X) * f = modetrans (f,X,X) by A1, Th6
.= f by LOPBAN_1:def_11 ; ::_thesis: verum
end;

theorem Th9: :: LOPBAN_2:9
for X being RealNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)
proof
let X be RealNormSpace; ::_thesis: for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)
let f, g, h be Element of BoundedLinearOperators (X,X); ::_thesis: f * (g + h) = (f * g) + (f * h)
set BLOP = R_NormSpace_of_BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set mf = modetrans (f,X,X);
set mg = modetrans (g,X,X);
set mh = modetrans (h,X,X);
set mgh = modetrans ((g + h),X,X);
 (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (f,X,X)) * (modetrans (g,X,X))),((modetrans (f,X,X)) * (modetrans (h,X,X)))) = (modetrans (f,X,X)) * (modetrans ((g + h),X,X))
proof
reconsider fh = (modetrans (f,X,X)) * (modetrans (h,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider k = (modetrans (f,X,X)) * (modetrans ((g + h),X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider hh = h as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: ( gg = modetrans (g,X,X) & hh = modetrans (h,X,X) ) by LOPBAN_1:def_11;
 for x being VECTOR of X holds ((modetrans (f,X,X)) * (modetrans ((g + h),X,X))) . x = (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + (((modetrans (f,X,X)) * (modetrans (h,X,X))) . x)
proof
let x be VECTOR of X; ::_thesis: ((modetrans (f,X,X)) * (modetrans ((g + h),X,X))) . x = (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + (((modetrans (f,X,X)) * (modetrans (h,X,X))) . x)
 ( g + h = gg + hh & modetrans ((g + h),X,X) = g + h ) by LOPBAN_1:def_11;
then A2: (modetrans ((g + h),X,X)) . x = ((modetrans (g,X,X)) . x) + ((modetrans (h,X,X)) . x) by A1, LOPBAN_1:35;
thus ((modetrans (f,X,X)) * (modetrans ((g + h),X,X))) . x = (modetrans (f,X,X)) . ((modetrans ((g + h),X,X)) . x) by Th4
.= ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x)) + ((modetrans (f,X,X)) . ((modetrans (h,X,X)) . x)) by A2, VECTSP_1:def_20
.= (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + ((modetrans (f,X,X)) . ((modetrans (h,X,X)) . x)) by Th4
.= (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + (((modetrans (f,X,X)) * (modetrans (h,X,X))) . x) by Th4 ; ::_thesis: verum
end;
then  k = fg + fh by LOPBAN_1:35;
hence  (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (f,X,X)) * (modetrans (g,X,X))),((modetrans (f,X,X)) * (modetrans (h,X,X)))) = (modetrans (f,X,X)) * (modetrans ((g + h),X,X)) ; ::_thesis: verum
end;
hence  f * (g + h) = (f * g) + (f * h) ; ::_thesis: verum
end;

theorem Th10: :: LOPBAN_2:10
for X being RealNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds (g + h) * f = (g * f) + (h * f)
proof
let X be RealNormSpace; ::_thesis: for f, g, h being Element of BoundedLinearOperators (X,X) holds (g + h) * f = (g * f) + (h * f)
let f, g, h be Element of BoundedLinearOperators (X,X); ::_thesis: (g + h) * f = (g * f) + (h * f)
set BLOP = R_NormSpace_of_BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set mf = modetrans (f,X,X);
set mg = modetrans (g,X,X);
set mh = modetrans (h,X,X);
set mgh = modetrans ((g + h),X,X);
 (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (g,X,X)) * (modetrans (f,X,X))),((modetrans (h,X,X)) * (modetrans (f,X,X)))) = (modetrans ((g + h),X,X)) * (modetrans (f,X,X))
proof
reconsider hf = (modetrans (h,X,X)) * (modetrans (f,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider gf = (modetrans (g,X,X)) * (modetrans (f,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider k = (modetrans ((g + h),X,X)) * (modetrans (f,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider hh = h as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: ( gg = modetrans (g,X,X) & hh = modetrans (h,X,X) ) by LOPBAN_1:def_11;
 for x being VECTOR of X holds ((modetrans ((g + h),X,X)) * (modetrans (f,X,X))) . x = (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + (((modetrans (h,X,X)) * (modetrans (f,X,X))) . x)
proof
let x be VECTOR of X; ::_thesis: ((modetrans ((g + h),X,X)) * (modetrans (f,X,X))) . x = (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + (((modetrans (h,X,X)) * (modetrans (f,X,X))) . x)
 ( g + h = gg + hh & modetrans ((g + h),X,X) = g + h ) by LOPBAN_1:def_11;
then A2: (modetrans ((g + h),X,X)) . ((modetrans (f,X,X)) . x) = ((modetrans (g,X,X)) . ((modetrans (f,X,X)) . x)) + ((modetrans (h,X,X)) . ((modetrans (f,X,X)) . x)) by A1, LOPBAN_1:35;
thus ((modetrans ((g + h),X,X)) * (modetrans (f,X,X))) . x = (modetrans ((g + h),X,X)) . ((modetrans (f,X,X)) . x) by Th4
.= (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + ((modetrans (h,X,X)) . ((modetrans (f,X,X)) . x)) by A2, Th4
.= (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + (((modetrans (h,X,X)) * (modetrans (f,X,X))) . x) by Th4 ; ::_thesis: verum
end;
then  k = gf + hf by LOPBAN_1:35;
hence  (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (g,X,X)) * (modetrans (f,X,X))),((modetrans (h,X,X)) * (modetrans (f,X,X)))) = (modetrans ((g + h),X,X)) * (modetrans (f,X,X)) ; ::_thesis: verum
end;
hence  (g + h) * f = (g * f) + (h * f) ; ::_thesis: verum
end;

theorem Th11: :: LOPBAN_2:11
for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X)
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
proof
let X be RealNormSpace; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X)
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
let a, b be Real; ::_thesis: (a * b) * (f * g) = (a * f) * (b * g)
set BLOP = R_NormSpace_of_BoundedLinearOperators (X,X);
set EXMULT = Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set mf = modetrans (f,X,X);
set mg = modetrans (g,X,X);
set maf = modetrans ((a * f),X,X);
set mbg = modetrans ((b * g),X,X);
 (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((a * b),((modetrans (f,X,X)) * (modetrans (g,X,X)))) = (modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))
proof
reconsider k = (modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9;
reconsider ff = f, gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: gg = modetrans (g,X,X) by LOPBAN_1:def_11;
A2: ff = modetrans (f,X,X) by LOPBAN_1:def_11;
 for x being VECTOR of X holds ((modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))) . x = (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x)
proof
let x be VECTOR of X; ::_thesis: ((modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))) . x = (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x)
set y = b * ((modetrans (g,X,X)) . x);
 ( a * f = a * ff & modetrans ((a * f),X,X) = a * f ) by LOPBAN_1:def_11;
then A3: (modetrans ((a * f),X,X)) . (b * ((modetrans (g,X,X)) . x)) = a * ((modetrans (f,X,X)) . (b * ((modetrans (g,X,X)) . x))) by A2, LOPBAN_1:36;
 ( b * g = b * gg & modetrans ((b * g),X,X) = b * g ) by LOPBAN_1:def_11;
then A4: (modetrans ((b * g),X,X)) . x = b * ((modetrans (g,X,X)) . x) by A1, LOPBAN_1:36;
thus ((modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))) . x = (modetrans ((a * f),X,X)) . ((modetrans ((b * g),X,X)) . x) by Th4
.= a * (b * ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x))) by A3, A4, LOPBAN_1:def_5
.= (a * b) * ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x)) by RLVECT_1:def_7
.= (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) by Th4 ; ::_thesis: verum
end;
then  k = (a * b) * fg by LOPBAN_1:36;
hence  (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((a * b),((modetrans (f,X,X)) * (modetrans (g,X,X)))) = (modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X)) ; ::_thesis: verum
end;
hence  (a * b) * (f * g) = (a * f) * (b * g) ; ::_thesis: verum
end;

theorem Th12: :: LOPBAN_2:12
for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X)
for a being Real holds a * (f * g) = (a * f) * g
proof
let X be RealNormSpace; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X)
for a being Real holds a * (f * g) = (a * f) * g
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: for a being Real holds a * (f * g) = (a * f) * g
let a be Real; ::_thesis: a * (f * g) = (a * f) * g
set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider gg = g as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
A1: 1 * g = 1 * gg
.= g by RLVECT_1:def_8 ;
a * (f * g) = (a * 1) * (f * g)
.= (a * f) * (1 * g) by Th11 ;
hence  a * (f * g) = (a * f) * g by A1; ::_thesis: verum
end;

definition
let X be RealNormSpace;
func Ring_of_BoundedLinearOperators X ->  doubleLoopStr  equals :: LOPBAN_2:def 6
 doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
correctness
coherence
doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) is doubleLoopStr ;
;
end;

:: deftheorem  defines Ring_of_BoundedLinearOperators LOPBAN_2:def_6_:_
 for X being RealNormSpace holds Ring_of_BoundedLinearOperators X = doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);

registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  non empty strict ;
coherence
 ( not Ring_of_BoundedLinearOperators X is empty & Ring_of_BoundedLinearOperators X is strict ) ;
end;

Lm1: now__::_thesis:_for_X_being_RealNormSpace
for_x,_e_being_Element_of_(Ring_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let X be RealNormSpace; ::_thesis: for x, e being Element of (Ring_of_BoundedLinearOperators X) st e = FuncUnit X holds
( x * e = x & e * x = x )
set F = Ring_of_BoundedLinearOperators X;
let x, e be Element of (Ring_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x & e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x & e * x = x )
hence x * e = f * (FuncUnit X) by Def4
.= x by Th8 ;
::_thesis: e * x = x
thus e * x = (FuncUnit X) * f by A1, Def4
.= x by Th8 ; ::_thesis: verum
end;

registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  unital ;
coherence
 Ring_of_BoundedLinearOperators X is unital
proof
reconsider e = FuncUnit X as Element of (Ring_of_BoundedLinearOperators X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (Ring_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (Ring_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm1; ::_thesis: verum
end;
end;

theorem Th13: :: LOPBAN_2:13
for X being RealNormSpace
for x, y, z being Element of (Ring_of_BoundedLinearOperators X) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof
let X be RealNormSpace; ::_thesis: for x, y, z being Element of (Ring_of_BoundedLinearOperators X) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
let x, y, z be Element of (Ring_of_BoundedLinearOperators X); ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
set RBLOP = Ring_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: ( x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x + (0. (Ring_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: ( ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus  ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) ::_thesis: ( (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
proof
consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (Ring_of_BoundedLinearOperators X) ;
take  t ; ::_thesis: x + t = 0. (Ring_of_BoundedLinearOperators X)
thus  x + t = 0. (Ring_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: ( x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (1. (Ring_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: ( (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus (1. (Ring_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: (y + z) * x = (y * x) + (z * 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;

theorem Th14: :: LOPBAN_2:14
for X being RealNormSpace holds Ring_of_BoundedLinearOperators X is Ring
proof
let X be RealNormSpace; ::_thesis: Ring_of_BoundedLinearOperators X is Ring
set R = Ring_of_BoundedLinearOperators X;
A1: Ring_of_BoundedLinearOperators X is right_complementable
proof
let x be Element of (Ring_of_BoundedLinearOperators X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
thus  ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) by Th13; :: according to ALGSTR_0:def_11 ::_thesis: verum
end;
 for x, y, z being Element of (Ring_of_BoundedLinearOperators X) holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by Th13;
hence  Ring_of_BoundedLinearOperators X is Ring by A1, GROUP_1:def_3, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, VECTSP_1:def_6, VECTSP_1:def_7; ::_thesis: verum
end;

registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed associative right_unital distributive left_unital ;
coherence
 ( Ring_of_BoundedLinearOperators X is Abelian & Ring_of_BoundedLinearOperators X is add-associative & Ring_of_BoundedLinearOperators X is right_zeroed & Ring_of_BoundedLinearOperators X is right_complementable & Ring_of_BoundedLinearOperators X is associative & Ring_of_BoundedLinearOperators X is left_unital & Ring_of_BoundedLinearOperators X is right_unital & Ring_of_BoundedLinearOperators X is distributive ) by Th14;
end;

definition
let X be RealNormSpace;
func R_Algebra_of_BoundedLinearOperators X ->  AlgebraStr  equals :: LOPBAN_2:def 7
 AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
correctness
coherence
AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) is AlgebraStr ;
;
end;

:: deftheorem  defines R_Algebra_of_BoundedLinearOperators LOPBAN_2:def_7_:_
 for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X = AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);

registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators X ->  non empty strict ;
coherence
 ( not R_Algebra_of_BoundedLinearOperators X is empty & R_Algebra_of_BoundedLinearOperators X is strict ) ;
end;

Lm2: now__::_thesis:_for_X_being_RealNormSpace
for_x,_e_being_Element_of_(R_Algebra_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let X be RealNormSpace; ::_thesis: for x, e being Element of (R_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds
( x * e = x & e * x = x )
set F = R_Algebra_of_BoundedLinearOperators X;
let x, e be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x & e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x & e * x = x )
hence x * e = f * (FuncUnit X) by Def4
.= x by Th8 ;
::_thesis: e * x = x
thus e * x = (FuncUnit X) * f by A1, Def4
.= x by Th8 ; ::_thesis: verum
end;

registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators X ->  unital ;
coherence
 R_Algebra_of_BoundedLinearOperators X is unital
proof
reconsider e = FuncUnit X as Element of (R_Algebra_of_BoundedLinearOperators X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm2; ::_thesis: verum
end;
end;

theorem :: LOPBAN_2:15
for X being RealNormSpace
for x, y, z being Element of (R_Algebra_of_BoundedLinearOperators X)
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
proof
let X be RealNormSpace; ::_thesis: for x, y, z being Element of (R_Algebra_of_BoundedLinearOperators X)
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
let a, b be Real; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
set RBLOP = R_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: ( x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus x + (0. (R_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: ( ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus  ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) ::_thesis: ( (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
proof
consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (R_Algebra_of_BoundedLinearOperators X) ;
take  t ; ::_thesis: x + t = 0. (R_Algebra_of_BoundedLinearOperators X)
thus  x + t = 0. (R_Algebra_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: ( x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: ( (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (1. (R_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: ( (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
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: ( a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus a * (x * y) = a * (xx * yy) by Def4
.= (a * xx) * yy by Th12
.= (a * x) * y by Def4 ; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by RLVECT_1:def_5
.= (a * x) + (a * y) ; ::_thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by RLVECT_1:def_6
.= (a * x) + (b * x) ; ::_thesis: ( (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (a * b) * x = (a * b) * f
.= a * (b * f) by RLVECT_1:def_7
.= a * (b * x) ; ::_thesis: (a * b) * (x * y) = (a * x) * (b * y)
thus (a * b) * (x * y) = (a * b) * (xx * yy) by Def4
.= (a * xx) * (b * yy) by Th11
.= (a * x) * (b * y) by Def4 ; ::_thesis: verum
end;

definition
mode BLAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative right-distributive right_unital AlgebraStr ;
end;

registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative associative right-distributive right_unital ;
coherence
 ( R_Algebra_of_BoundedLinearOperators X is Abelian & R_Algebra_of_BoundedLinearOperators X is add-associative & R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
set A = R_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
thus  R_Algebra_of_BoundedLinearOperators X is Abelian ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is add-associative & R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider f = x, g = y as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is add-associative ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is right_zeroed ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + (0. (R_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is right_complementable ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (R_Algebra_of_BoundedLinearOperators X) ;
take  t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (R_Algebra_of_BoundedLinearOperators X)
thus  x + t = 0. (R_Algebra_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is associative ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is right_unital ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_4 ::_thesis: x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x
reconsider xx = x as Element of BoundedLinearOperators (X,X) ;
thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is right-distributive ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is vector-distributive ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let a be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: a * (x + y) = (a * x) + (a * y)
reconsider f = x, g = y as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by RLVECT_1:def_5
.= (a * x) + (a * y) ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is scalar-distributive ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let a, b be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds (a + b) * b1 = (a * b1) + (b * b1)
let x be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: (a + b) * x = (a * x) + (b * x)
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by RLVECT_1:def_6
.= (a * x) + (b * x) ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is scalar-associative ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let a, b be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds (a * b) * b1 = a * (b * b1)
let x be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: (a * b) * x = a * (b * x)
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (a * b) * x = (a * b) * f
.= a * (b * f) by RLVECT_1:def_7
.= a * (b * x) ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is vector-associative ::_thesis: R_Algebra_of_BoundedLinearOperators X is strict
proof
let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to FUNCSDOM:def_9 ::_thesis: for b1 being Element of REAL holds b1 * (x * y) = (b1 * x) * y
let a be Real; ::_thesis: a * (x * y) = (a * x) * y
reconsider xx = x, yy = y as Element of BoundedLinearOperators (X,X) ;
thus a * (x * y) = a * (xx * yy) by Def4
.= (a * xx) * yy by Th12
.= (a * x) * y by Def4 ; ::_thesis: verum
end;
thus  R_Algebra_of_BoundedLinearOperators X is strict ; ::_thesis: verum
end;
end;

theorem :: LOPBAN_2:16
for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X is BLAlgebra ;

registration
cluster l1_Space  ->  complete ;
coherence
 l1_Space is complete
proof
thus  for vseq being sequence of l1_Space st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent by RSSPACE3:9; :: according to LOPBAN_1:def_15 ::_thesis: verum
end;
end;

registration
cluster l1_Space  ->  non trivial ;
coherence
 not l1_Space is trivial
proof
set a = 1 / 2;
reconsider x = (1 / 2) GeoSeq as Real_Sequence ;
A1: abs (1 / 2) = 1 / 2 by ABSVALUE:def_1;
defpred S1[ Element of NAT ] means  0 <= x . c1;
A2: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
A3: x . (n + 1) = (x . n) * (1 / 2) by PREPOWER:3;
assume  S1[n] ; ::_thesis: S1[n + 1]
hence  S1[n + 1] by A3; ::_thesis: verum
end;
A4: S1[ 0 ] by PREPOWER:3;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
then  x is absolutely_summable by A1, SERIES_1:24, SERIES_1:36;
then  seq_id x is absolutely_summable by RSSPACE:1;
then reconsider v = x as VECTOR of l1_Space by RSSPACE3:6;
(seq_id v) . 0 = x . 0 by RSSPACE:1
.= 1 by PREPOWER:3 ;
then  v <> Zeroseq by RSSPACE:def_6;
hence  not l1_Space is trivial by RSSPACE3:6, STRUCT_0:def_18; ::_thesis: verum
end;
end;

registration
cluster non empty non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like complete for NORMSTR ;
existence
 not for b1 being RealBanachSpace holds b1 is trivial
proof
take  l1_Space ; ::_thesis: not l1_Space is trivial
thus  not l1_Space is trivial ; ::_thesis: verum
end;
end;

theorem Th17: :: LOPBAN_2:17
for X being non trivial RealNormSpace ex w being VECTOR of X st ||.w.|| = 1
proof
let X be non trivial RealNormSpace; ::_thesis: ex w being VECTOR of X st ||.w.|| = 1
consider v being VECTOR of X such that
A1: v <> 0. X by STRUCT_0:def_18;
set a = ||.v.||;
reconsider w = (||.v.|| ") * v as VECTOR of X ;
take  w ; ::_thesis: ||.w.|| = 1
A2: ||.v.|| <> 0 by A1, NORMSP_0:def_5;
then A3: 0 < ||.v.|| by NORMSP_1:4;
A4: abs (||.v.|| ") = abs (1 * (||.v.|| "))
.= abs (1 / ||.v.||) by XCMPLX_0:def_9
.= 1 / (abs ||.v.||) by ABSVALUE:7
.= 1 * ((abs ||.v.||) ") by XCMPLX_0:def_9
.= ||.v.|| " by A3, ABSVALUE:def_1 ;
thus ||.w.|| = (abs (||.v.|| ")) * ||.v.|| by NORMSP_1:def_1
.= 1 by A2, A4, XCMPLX_0:def_7 ; ::_thesis: verum
end;

theorem Th18: :: LOPBAN_2:18
for X being non trivial RealNormSpace holds (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1
proof
let X be non trivial RealNormSpace; ::_thesis: (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1
consider v being VECTOR of X such that
A1: ||.v.|| = 1 by Th17;
reconsider ii = id the carrier of X as Lipschitzian LinearOperator of X,X by Th3;
A2: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_ii_holds_
r_<=_1
let r be Real; ::_thesis: ( r in PreNorms ii implies r <= 1 )
assume  r in PreNorms ii ; ::_thesis: r <= 1
then  ex t being VECTOR of X st
( r = ||.(ii . t).|| & ||.t.|| <= 1 ) ;
hence  r <= 1 by FUNCT_1:18; ::_thesis: verum
end;
 ii . v = v by FUNCT_1:18;
then A3: 1 in  {  ||.(ii . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  by A1;
 ( not PreNorms ii is empty & PreNorms ii is bounded_above ) by LOPBAN_1:27;
then A4: 1 <= upper_bound (PreNorms ii) by A3, SEQ_4:def_1;
 ( ( for s being real number st s in PreNorms ii holds
s <= 1 ) implies upper_bound (PreNorms ii) <= 1 ) by SEQ_4:45;
then  upper_bound (PreNorms ii) = 1 by A2, A4, XXREAL_0:1;
hence  (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1 by LOPBAN_1:30; ::_thesis: verum
end;

definition
attrc1 is strict ;
struct Normed_AlgebraStr  ->  AlgebraStr , NORMSTR ;
aggrNormed_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) ->  Normed_AlgebraStr ;
end;

registration
cluster non empty for Normed_AlgebraStr ;
existence
 not for b1 being Normed_AlgebraStr holds b1 is empty
proof
set A = the non empty set ;
set m = the BinOp of the non empty set ;
set a = the BinOp of the non empty set ;
set M = the Function of [:REAL, the non empty set :], the non empty set ;
set U = the Element of the non empty set ;
set Z = the Element of the non empty set ;
set n = the Function of the non empty set ,REAL;
take  Normed_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set , the Function of the non empty set ,REAL #) ; ::_thesis: not Normed_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set , the Function of the non empty set ,REAL #) is empty
thus  not the carrier of Normed_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set , the Function of the non empty set ,REAL #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
let X be RealNormSpace;
func R_Normed_Algebra_of_BoundedLinearOperators X ->  Normed_AlgebraStr  equals :: LOPBAN_2:def 8
 Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);
correctness
coherence
Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #) is Normed_AlgebraStr ;
;
end;

:: deftheorem  defines R_Normed_Algebra_of_BoundedLinearOperators LOPBAN_2:def_8_:_
 for X being RealNormSpace holds R_Normed_Algebra_of_BoundedLinearOperators X = Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);

registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  non empty strict ;
coherence
 ( not R_Normed_Algebra_of_BoundedLinearOperators X is empty & R_Normed_Algebra_of_BoundedLinearOperators X is strict ) ;
end;

Lm3: now__::_thesis:_for_X_being_RealNormSpace
for_x,_e_being_Element_of_(R_Normed_Algebra_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_
(_x_*_e_=_x_&_e_*_x_=_x_)
let X be RealNormSpace; ::_thesis: for x, e being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds
( x * e = x & e * x = x )
set F = R_Normed_Algebra_of_BoundedLinearOperators X;
let x, e be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x & e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x & e * x = x )
hence x * e = f * (FuncUnit X) by Def4
.= x by Th8 ;
::_thesis: e * x = x
thus e * x = (FuncUnit X) * f by A1, Def4
.= x by Th8 ; ::_thesis: verum
end;

registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  unital ;
coherence
 R_Normed_Algebra_of_BoundedLinearOperators X is unital
proof
reconsider e = FuncUnit X as Element of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm3; ::_thesis: verum
end;
end;

theorem Th19: :: LOPBAN_2:19
for X being RealNormSpace
for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being real number 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 )
proof
let X be RealNormSpace; ::_thesis: for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being real number 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 )
let x, y, z be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: for a, b being real number 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 )
let a, b be real number ; ::_thesis: ( 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 )
reconsider a1 = a, b1 = b as Real by XREAL_0:def_1;
set RBLOP = R_Normed_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: ( (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 )
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: ( 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 )
thus x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: ( 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 )
thus  ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ::_thesis: ( (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 )
proof
consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (R_Normed_Algebra_of_BoundedLinearOperators X) ;
take  t ; ::_thesis: x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X)
thus  x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: ( 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 )
thus x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: ( (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 )
thus (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; ::_thesis: ( 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 )
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: ( (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 )
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: ( 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 )
thus a * (x * y) = a1 * (xx * yy) by Def4
.= (a1 * xx) * yy by Th12
.= (a * x) * y by Def4 ; ::_thesis: ( (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 )
thus (a * b) * (x * y) = (a1 * b1) * (xx * yy) by Def4
.= (a1 * xx) * (b1 * yy) by Th11
.= (a * x) * (b * y) by Def4 ; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x )
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by RLVECT_1:def_5
.= (a * x) + (a * y) ; ::_thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x )
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by RLVECT_1:def_6
.= (a * x) + (b * x) ; ::_thesis: ( (a * b) * x = a * (b * x) & 1 * x = x )
thus (a * b) * x = (a * b) * f
.= a * (b * f) by RLVECT_1:def_7
.= a * (b * x) ; ::_thesis: 1 * x = x
thus 1 * x = 1 * f
.= x by RLVECT_1:def_8 ; ::_thesis: verum
end;

theorem Th20: :: LOPBAN_2:20
for X being RealNormSpace holds
( 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 )
proof
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).||_=_(abs_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).|| = (abs 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).|| = (abs 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).|| = (abs 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).|| = (abs a) * ||.x.||
thus ||.(a * x).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,x))
.= ||.(a * x1).||
.= (abs 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;
A6: ( ( for a, b being real number
for v being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds (a + b) * v = (a * v) + (b * v) ) & ( for a, b being real number
for v being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds (a * b) * v = a * (b * v) ) ) by Th19;
 ( ( 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 number
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, A6, A2, FUNCSDOM:def_9, GROUP_1:def_3, NORMSP_0:def_5, NORMSP_1:def_1, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8, VECTSP_1:def_2, VECTSP_1:def_4; ::_thesis: verum
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital strict for Normed_AlgebraStr ;
existence
 ex b1 being non empty Normed_AlgebraStr st
( b1 is reflexive & b1 is discerning & b1 is RealNormSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is right_unital & b1 is right-distributive & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is vector-associative & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is strict )
proof
set X = the RealNormSpace;
take  R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace ; ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is reflexive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is discerning & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is Abelian & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is add-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is strict )
thus  ( R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is reflexive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is discerning & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is Abelian & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is add-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is strict ) by Th20; ::_thesis: verum
end;
end;

definition
mode Normed_Algebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Normed_AlgebraStr ;
end;

registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital ;
correctness
coherence
( 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 scalar-unital );
by Th20;
end;

definition
let X be non empty Normed_AlgebraStr ;
attrX is Banach_Algebra-like_1  means :: LOPBAN_2:def 9
 for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||;
attrX is Banach_Algebra-like_2  means :Def10: :: LOPBAN_2:def 10
||.(1. X).|| = 1;
attrX is Banach_Algebra-like_3  means :: LOPBAN_2:def 11
 for a being Real
for x, y being Element of X holds a * (x * y) = x * (a * y);
end;

:: deftheorem  defines Banach_Algebra-like_1 LOPBAN_2:def_9_:_
 for X being non empty Normed_AlgebraStr holds
( X is Banach_Algebra-like_1 iff for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.|| );

:: deftheorem Def10 defines Banach_Algebra-like_2 LOPBAN_2:def_10_:_
 for X being non empty Normed_AlgebraStr holds
( X is Banach_Algebra-like_2 iff ||.(1. X).|| = 1 );

:: deftheorem  defines Banach_Algebra-like_3 LOPBAN_2:def_11_:_
 for X being non empty Normed_AlgebraStr holds
( X is Banach_Algebra-like_3 iff for a being Real
for x, y being Element of X holds a * (x * y) = x * (a * y) );

definition
let X be Normed_Algebra;
attrX is Banach_Algebra-like  means :Def12: :: LOPBAN_2:def 12
( X is Banach_Algebra-like_1 & X is Banach_Algebra-like_2 & X is Banach_Algebra-like_3 & X is left_unital & X is left-distributive & X is complete );
end;

:: deftheorem Def12 defines Banach_Algebra-like LOPBAN_2:def_12_:_
 for X being Normed_Algebra holds
( X is Banach_Algebra-like iff ( X is Banach_Algebra-like_1 & X is Banach_Algebra-like_2 & X is Banach_Algebra-like_3 & X is left_unital & X is left-distributive & X is complete ) );

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Banach_Algebra-like  ->  left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 for Normed_AlgebraStr ;
coherence
 for b1 being Normed_Algebra st b1 is Banach_Algebra-like holds
( b1 is Banach_Algebra-like_1 & b1 is Banach_Algebra-like_2 & b1 is Banach_Algebra-like_3 & b1 is left-distributive & b1 is left_unital & b1 is complete ) by Def12;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive left-distributive right_unital left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3  ->  Banach_Algebra-like for Normed_AlgebraStr ;
coherence
 for b1 being Normed_Algebra st b1 is Banach_Algebra-like_1 & b1 is Banach_Algebra-like_2 & b1 is Banach_Algebra-like_3 & b1 is left-distributive & b1 is left_unital & b1 is complete holds
b1 is Banach_Algebra-like by Def12;
end;

registration
let X be non trivial RealBanachSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  Banach_Algebra-like ;
coherence
 R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like
proof
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 by Def10; ::_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_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seq1_._n)_-_(seq1_._m)).||_<_r
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, RSSPACE3:8;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seq1_._n)_-_(seq1_._m)).||_<_r
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)) . ((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 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 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 Element of NAT st
for n being Element of 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_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((seq_._n)_-_g).||_<_r
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__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((seq_._n)_-_g).||_<_r
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)) . ((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 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 NORMSP_1:def_6; ::_thesis: verum
end;
hence  R_Normed_Algebra_of_BoundedLinearOperators X is complete by LOPBAN_1:def_15; ::_thesis: verum
end;
end;

registration
cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Banach_Algebra-like for Normed_AlgebraStr ;
existence
 ex b1 being Normed_Algebra st b1 is Banach_Algebra-like
proof
set X = the non trivial RealBanachSpace;
take  R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace ; ::_thesis: R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace is Banach_Algebra-like
thus  R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace is Banach_Algebra-like ; ::_thesis: verum
end;
end;

definition
mode Banach_Algebra is Banach_Algebra-like Normed_Algebra;
end;

theorem :: LOPBAN_2:21
for X being RealNormSpace holds 1. (Ring_of_BoundedLinearOperators X) = FuncUnit X ;

theorem :: LOPBAN_2:22
for X being RealNormSpace holds 1. (R_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;

theorem :: LOPBAN_2:23
for X being RealNormSpace holds 1. (R_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;