:: LOPBAN_1 semantic presentation

begin

definition
let X be set ;
let Y be non empty set ;
let F be Function of [:REAL,Y:],Y;
let a be real number ;
let f be Function of X,Y;
:: original: [;]
redefine funcF [;] (a,f) ->  Element of Funcs (X,Y);
coherence
 F [;] (a,f) is Element of Funcs (X,Y)
proof
A1: dom f = X by FUNCT_2:def_1;
 a in REAL by XREAL_0:def_1;
then  (dom f) --> a is Function of X,REAL by A1, FUNCOP_1:45;
then reconsider g = <:((dom f) --> a),f:> as Function of X,[:REAL,Y:] by FUNCT_3:58;
 F [;] (a,f) = F * g by FUNCOP_1:def_5;
hence  F [;] (a,f) is Element of Funcs (X,Y) by FUNCT_2:8; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let Y be non empty addLoopStr ;
func FuncAdd (X,Y) ->  BinOp of (Funcs (X, the carrier of Y)) means :Def1: :: LOPBAN_1:def 1
 for f, g being Element of Funcs (X, the carrier of Y) holds it . (f,g) = the addF of Y .: (f,g);
existence
 ex b1 being BinOp of (Funcs (X, the carrier of Y)) st
for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g)
proof
deffunc H1( Element of Funcs (X, the carrier of Y), Element of Funcs (X, the carrier of Y)) ->  Element of Funcs (X, the carrier of Y) = the addF of Y .: ($1,$2);
thus  ex ADD being BinOp of (Funcs (X, the carrier of Y)) st
for f, g being Element of Funcs (X, the carrier of Y) holds ADD . (f,g) = H1(f,g) from BINOP_1:sch_4(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being BinOp of (Funcs (X, the carrier of Y)) st ( for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of Y) holds b2 . (f,g) = the addF of Y .: (f,g) ) holds
b1 = b2
proof
let it1, it2 be BinOp of (Funcs (X, the carrier of Y)); ::_thesis: ( ( for f, g being Element of Funcs (X, the carrier of Y) holds it1 . (f,g) = the addF of Y .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of Y) holds it2 . (f,g) = the addF of Y .: (f,g) ) implies it1 = it2 )
assume that
A1: for f, g being Element of Funcs (X, the carrier of Y) holds it1 . (f,g) = the addF of Y .: (f,g) and
A2: for f, g being Element of Funcs (X, the carrier of Y) holds it2 . (f,g) = the addF of Y .: (f,g) ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_Funcs_(X,_the_carrier_of_Y)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of Funcs (X, the carrier of Y); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = the addF of Y .: (f,g) by A1
.= it2 . (f,g) by A2 ; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines FuncAdd LOPBAN_1:def_1_:_
 for X being non empty set
for Y being non empty addLoopStr
for b3 being BinOp of (Funcs (X, the carrier of Y)) holds
( b3 = FuncAdd (X,Y) iff for f, g being Element of Funcs (X, the carrier of Y) holds b3 . (f,g) = the addF of Y .: (f,g) );

definition
let X be non empty set ;
let Y be RealLinearSpace;
func FuncExtMult (X,Y) ->  Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) means :Def2: :: LOPBAN_1:def 2
 for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it . [a,f]) . x = a * (f . x);
existence
 ex b1 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x)
proof
deffunc H1( Real, Element of Funcs (X, the carrier of Y)) ->  Element of Funcs (X, the carrier of Y) = the Mult of Y [;] ($1,$2);
consider F being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) such that
A1: for a being Real
for f being Element of Funcs (X, the carrier of Y) holds F . (a,f) = H1(a,f) from BINOP_1:sch_4();
take  F ; ::_thesis: for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (F . [a,f]) . x = a * (f . x)
let a be Real; ::_thesis: for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (F . [a,f]) . x = a * (f . x)
let f be Element of Funcs (X, the carrier of Y); ::_thesis: for x being Element of X holds (F . [a,f]) . x = a * (f . x)
let x be Element of X; ::_thesis: (F . [a,f]) . x = a * (f . x)
A2: dom (F . [a,f]) = X by FUNCT_2:92;
 F . (a,f) = the Mult of Y [;] (a,f) by A1;
hence  (F . [a,f]) . x = a * (f . x) by A2, FUNCOP_1:32; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b2 . [a,f]) . x = a * (f . x) ) holds
b1 = b2
proof
let it1, it2 be Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)); ::_thesis: ( ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it1 . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it2 . [a,f]) . x = a * (f . x) ) implies it1 = it2 )
assume that
A3: for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it1 . [a,f]) . x = a * (f . x) and
A4: for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it2 . [a,f]) . x = a * (f . x) ; ::_thesis: it1 = it2
now__::_thesis:_for_a_being_Element_of_REAL_
for_f_being_Element_of_Funcs_(X,_the_carrier_of_Y)_holds_it1_._(a,f)_=_it2_._(a,f)
let a be Element of REAL ; ::_thesis: for f being Element of Funcs (X, the carrier of Y) holds it1 . (a,f) = it2 . (a,f)
let f be Element of Funcs (X, the carrier of Y); ::_thesis: it1 . (a,f) = it2 . (a,f)
now__::_thesis:_for_x_being_Element_of_X_holds_(it1_._[a,f])_._x_=_(it2_._[a,f])_._x
let x be Element of X; ::_thesis: (it1 . [a,f]) . x = (it2 . [a,f]) . x
thus (it1 . [a,f]) . x = a * (f . x) by A3
.= (it2 . [a,f]) . x by A4 ; ::_thesis: verum
end;
hence  it1 . (a,f) = it2 . (a,f) by FUNCT_2:63; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def_2_:_
 for X being non empty set
for Y being RealLinearSpace
for b3 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) holds
( b3 = FuncExtMult (X,Y) iff for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b3 . [a,f]) . x = a * (f . x) );

definition
let X be set ;
let Y be non empty ZeroStr ;
func FuncZero (X,Y) ->  Element of Funcs (X, the carrier of Y) equals :: LOPBAN_1:def 3
X --> (0. Y);
coherence
 X --> (0. Y) is Element of Funcs (X, the carrier of Y) by FUNCT_2:8;
end;

:: deftheorem  defines FuncZero LOPBAN_1:def_3_:_
 for X being set
for Y being non empty ZeroStr holds FuncZero (X,Y) = X --> (0. Y);

     Lm1:  for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
proof
let A, B be non empty set ; ::_thesis: for x being Element of A
for f being Function of A,B holds x in dom f
let x be Element of A; ::_thesis: for f being Function of A,B holds x in dom f
let f be Function of A,B; ::_thesis: x in dom f
 x in A ;
hence  x in dom f by FUNCT_2:def_1; ::_thesis: verum
end;

theorem Th1: :: LOPBAN_1:1
for X being non empty set
for Y being non empty addLoopStr
for f, g, h being Element of Funcs (X, the carrier of Y) holds
( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof
let X be non empty set ; ::_thesis: for Y being non empty addLoopStr
for f, g, h being Element of Funcs (X, the carrier of Y) holds
( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )
let Y be non empty addLoopStr ; ::_thesis: for f, g, h being Element of Funcs (X, the carrier of Y) holds
( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )
let f, g, h be Element of Funcs (X, the carrier of Y); ::_thesis: ( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )
hereby  ::_thesis: ( ( for x being Element of X holds h . x = (f . x) + (g . x) ) implies h = (FuncAdd (X,Y)) . (f,g) )
assume A1: h = (FuncAdd (X,Y)) . (f,g) ; ::_thesis: for x being Element of X holds h . x = (f . x) + (g . x)
let x be Element of X; ::_thesis: h . x = (f . x) + (g . x)
A2: x in dom ( the addF of Y .: (f,g)) by Lm1;
thus h . x = ( the addF of Y .: (f,g)) . x by A1, Def1
.= (f . x) + (g . x) by A2, FUNCOP_1:22 ; ::_thesis: verum
end;
assume A3: for x being Element of X holds h . x = (f . x) + (g . x) ; ::_thesis: h = (FuncAdd (X,Y)) . (f,g)
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(f,g))_._x_=_h_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (f,g)) . x = h . x
A4: x in dom ( the addF of Y .: (f,g)) by Lm1;
thus ((FuncAdd (X,Y)) . (f,g)) . x = ( the addF of Y .: (f,g)) . x by Def1
.= (f . x) + (g . x) by A4, FUNCOP_1:22
.= h . x by A3 ; ::_thesis: verum
end;
hence  h = (FuncAdd (X,Y)) . (f,g) by FUNCT_2:63; ::_thesis: verum
end;


theorem Th2: :: LOPBAN_1:2
for X being non empty set
for Y being RealLinearSpace
for h, f being Element of Funcs (X, the carrier of Y)
for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for h, f being Element of Funcs (X, the carrier of Y)
for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let Y be RealLinearSpace; ::_thesis: for h, f being Element of Funcs (X, the carrier of Y)
for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let h, f be Element of Funcs (X, the carrier of Y); ::_thesis: for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let a be Real; ::_thesis: ( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
thus  ( h = (FuncExtMult (X,Y)) . [a,f] implies for x being Element of X holds h . x = a * (f . x) ) by Def2; ::_thesis: ( ( for x being Element of X holds h . x = a * (f . x) ) implies h = (FuncExtMult (X,Y)) . [a,f] )
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h_._x_=_a_*_(f_._x)_)_implies_h_=_(FuncExtMult_(X,Y))_._[a,f]_)
assume A1: for x being Element of X holds h . x = a * (f . x) ; ::_thesis: h = (FuncExtMult (X,Y)) . [a,f]
 for x being Element of X holds h . x = ((FuncExtMult (X,Y)) . [a,f]) . x
proof
let x be Element of X; ::_thesis: h . x = ((FuncExtMult (X,Y)) . [a,f]) . x
thus h . x = a * (f . x) by A1
.= ((FuncExtMult (X,Y)) . [a,f]) . x by Def2 ; ::_thesis: verum
end;
hence  h = (FuncExtMult (X,Y)) . [a,f] by FUNCT_2:63; ::_thesis: verum
end;
hence  ( ( for x being Element of X holds h . x = a * (f . x) ) implies h = (FuncExtMult (X,Y)) . [a,f] ) ; ::_thesis: verum
end;


theorem Th3: :: LOPBAN_1:3
for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
let Y be RealLinearSpace; ::_thesis: for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
let f, g be Element of Funcs (X, the carrier of Y); ::_thesis: (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(f,g))_._x_=_((FuncAdd_(X,Y))_._(g,f))_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (f,g)) . x = ((FuncAdd (X,Y)) . (g,f)) . x
thus ((FuncAdd (X,Y)) . (f,g)) . x = (g . x) + (f . x) by Th1
.= ((FuncAdd (X,Y)) . (g,f)) . x by Th1 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th4: :: LOPBAN_1:4
for X being non empty set
for Y being RealLinearSpace
for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
let Y be RealLinearSpace; ::_thesis: for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
let f, g, h be Element of Funcs (X, the carrier of Y); ::_thesis: (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(f,((FuncAdd_(X,Y))_._(g,h))))_._x_=_((FuncAdd_(X,Y))_._(((FuncAdd_(X,Y))_._(f,g)),h))_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h)))) . x = ((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)) . x
thus ((FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h)))) . x = (f . x) + (((FuncAdd (X,Y)) . (g,h)) . x) by Th1
.= (f . x) + ((g . x) + (h . x)) by Th1
.= ((f . x) + (g . x)) + (h . x) by RLVECT_1:def_3
.= (((FuncAdd (X,Y)) . (f,g)) . x) + (h . x) by Th1
.= ((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)) . x by Th1 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th5: :: LOPBAN_1:5
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f
let Y be RealLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f
let f be Element of Funcs (X, the carrier of Y); ::_thesis: (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._((FuncZero_(X,Y)),f))_._x_=_f_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . ((FuncZero (X,Y)),f)) . x = f . x
thus ((FuncAdd (X,Y)) . ((FuncZero (X,Y)),f)) . x = ((FuncZero (X,Y)) . x) + (f . x) by Th1
.= (0. Y) + (f . x) by FUNCOP_1:7
.= f . x by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f by FUNCT_2:63; ::_thesis: verum
end;

theorem Th6: :: LOPBAN_1:6
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
let Y be RealLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
let f be Element of Funcs (X, the carrier of Y); ::_thesis: (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(f,((FuncExtMult_(X,Y))_._[(-_1),f])))_._x_=_(FuncZero_(X,Y))_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f]))) . x = (FuncZero (X,Y)) . x
set y = f . x;
thus ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f]))) . x = (f . x) + (((FuncExtMult (X,Y)) . [(- 1),f]) . x) by Th1
.= (f . x) + ((- 1) * (f . x)) by Th2
.= (f . x) + (- (f . x)) by RLVECT_1:16
.= 0. Y by RLVECT_1:5
.= (FuncZero (X,Y)) . x by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th7: :: LOPBAN_1:7
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1,f] = f
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1,f] = f
let Y be RealLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1,f] = f
let f be Element of Funcs (X, the carrier of Y); ::_thesis: (FuncExtMult (X,Y)) . [1,f] = f
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncExtMult_(X,Y))_._[1,f])_._x_=_f_._x
let x be Element of X; ::_thesis: ((FuncExtMult (X,Y)) . [1,f]) . x = f . x
thus ((FuncExtMult (X,Y)) . [1,f]) . x = 1 * (f . x) by Th2
.= f . x by RLVECT_1:def_8 ; ::_thesis: verum
end;
hence  (FuncExtMult (X,Y)) . [1,f] = f by FUNCT_2:63; ::_thesis: verum
end;

theorem Th8: :: LOPBAN_1:8
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
let Y be RealLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
let f be Element of Funcs (X, the carrier of Y); ::_thesis: for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
let a, b be Real; ::_thesis: (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncExtMult_(X,Y))_._[a,((FuncExtMult_(X,Y))_._[b,f])])_._x_=_((FuncExtMult_(X,Y))_._[(a_*_b),f])_._x
let x be Element of X; ::_thesis: ((FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])]) . x = ((FuncExtMult (X,Y)) . [(a * b),f]) . x
thus ((FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])]) . x = a * (((FuncExtMult (X,Y)) . [b,f]) . x) by Th2
.= a * (b * (f . x)) by Th2
.= (a * b) * (f . x) by RLVECT_1:def_7
.= ((FuncExtMult (X,Y)) . [(a * b),f]) . x by Th2 ; ::_thesis: verum
end;
hence  (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f] by FUNCT_2:63; ::_thesis: verum
end;

theorem Th9: :: LOPBAN_1:9
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let Y be RealLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let f be Element of Funcs (X, the carrier of Y); ::_thesis: for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let a, b be Real; ::_thesis: (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(((FuncExtMult_(X,Y))_._[a,f]),((FuncExtMult_(X,Y))_._[b,f])))_._x_=_((FuncExtMult_(X,Y))_._[(a_+_b),f])_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f]))) . x = ((FuncExtMult (X,Y)) . [(a + b),f]) . x
thus ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f]))) . x = (((FuncExtMult (X,Y)) . [a,f]) . x) + (((FuncExtMult (X,Y)) . [b,f]) . x) by Th1
.= (a * (f . x)) + (((FuncExtMult (X,Y)) . [b,f]) . x) by Th2
.= (a * (f . x)) + (b * (f . x)) by Th2
.= (a + b) * (f . x) by RLVECT_1:def_6
.= ((FuncExtMult (X,Y)) . [(a + b),f]) . x by Th2 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f] by FUNCT_2:63; ::_thesis: verum
end;

Lm2:  for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
let Y be RealLinearSpace; ::_thesis: for f, g being Element of Funcs (X, the carrier of Y)
for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
let f, g be Element of Funcs (X, the carrier of Y); ::_thesis: for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
let a be Real; ::_thesis: (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(((FuncExtMult_(X,Y))_._[a,f]),((FuncExtMult_(X,Y))_._[a,g])))_._x_=_((FuncExtMult_(X,Y))_._[a,((FuncAdd_(X,Y))_._(f,g))])_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g]))) . x = ((FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]) . x
thus ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g]))) . x = (((FuncExtMult (X,Y)) . [a,f]) . x) + (((FuncExtMult (X,Y)) . [a,g]) . x) by Th1
.= (a * (f . x)) + (((FuncExtMult (X,Y)) . [a,g]) . x) by Th2
.= (a * (f . x)) + (a * (g . x)) by Th2
.= a * ((f . x) + (g . x)) by RLVECT_1:def_5
.= a * (((FuncAdd (X,Y)) . (f,g)) . x) by Th1
.= ((FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]) . x by Th2 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))] by FUNCT_2:63; ::_thesis: verum
end;

theorem Th10: :: LOPBAN_1:10
for X being non empty set
for Y being RealLinearSpace holds RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace
proof
let X be non empty set ; ::_thesis: for Y being RealLinearSpace holds RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace
let Y be RealLinearSpace; ::_thesis: RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace
A1: for a, b being real number
for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a * b) * v = a * (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
 for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a * b) * v = a * (b * v) by Th8;
hence  for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
A2: for a, b being real number
for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a + b) * v = (a * v) + (b * v)
proof
let a, b be real number ; ::_thesis: for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
 for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a + b) * v = (a * v) + (b * v) by Th9;
hence  for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
set IT = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);
A3: for u, v, w being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (u + v) + w = u + (v + w) by Th4;
A4: RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is right_complementable
proof
let u be VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); :: according to ALGSTR_0:def_16 ::_thesis: u is right_complementable
reconsider u9 = u as Element of Funcs (X, the carrier of Y) ;
reconsider w = (FuncExtMult (X,Y)) . [(- 1),u9] as VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) ;
take  w ; :: according to ALGSTR_0:def_11 ::_thesis: u + w = 0. RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)
thus  u + w = 0. RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) by Th6; ::_thesis: verum
end;
A5: for a being real number
for u, v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds a * (u + v) = (a * u) + (a * v)
proof
let a be real number ; ::_thesis: for u, v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds a * (u + v) = (a * u) + (a * v)
reconsider a = a as Real by XREAL_0:def_1;
 for u, v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds a * (u + v) = (a * u) + (a * v) by Lm2;
hence  for u, v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds a * (u + v) = (a * u) + (a * v) ; ::_thesis: verum
end;
A6: for v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds 1 * v = v by Th7;
A7: for u being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds u + (0. RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)) = u
proof
let u be VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); ::_thesis: u + (0. RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)) = u
reconsider u9 = u as Element of Funcs (X, the carrier of Y) ;
thus u + (0. RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)) = (FuncAdd (X,Y)) . ((FuncZero (X,Y)),u9) by Th3
.= u by Th5 ; ::_thesis: verum
end;
 for u, v being VECTOR of RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds u + v = v + u by Th3;
hence  RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace by A3, A7, A4, A5, A2, A1, A6, 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; ::_thesis: verum
end;

definition
let X be non empty set ;
let Y be RealLinearSpace;
func RealVectSpace (X,Y) ->  RealLinearSpace equals :: LOPBAN_1:def 4
 RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);
coherence
 RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace by Th10;
end;

:: deftheorem  defines RealVectSpace LOPBAN_1:def_4_:_
 for X being non empty set
for Y being RealLinearSpace holds RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);

registration
let X be non empty set ;
let Y be RealLinearSpace;
cluster RealVectSpace (X,Y) ->  strict ;
coherence
 RealVectSpace (X,Y) is strict ;
end;

registration
let X be non empty set ;
let Y be RealLinearSpace;
cluster RealVectSpace (X,Y) ->  constituted-Functions ;
coherence
 RealVectSpace (X,Y) is constituted-Functions by MONOID_0:80;
end;

definition
let X be non empty set ;
let Y be RealLinearSpace;
let f be VECTOR of (RealVectSpace (X,Y));
let x be Element of X;
:: original: .
redefine funcf . x ->  VECTOR of Y;
coherence
 f . x is VECTOR of Y
proof
consider g being Function such that
A1: f = g and
A2: dom g = X and
A3: rng g c= the carrier of Y by FUNCT_2:def_2;
 f . x in rng g by A1, A2, FUNCT_1:def_3;
hence  f . x is VECTOR of Y by A3; ::_thesis: verum
end;
end;

theorem :: LOPBAN_1:11
for X being non empty set
for Y being RealLinearSpace
for f, g, h being VECTOR of (RealVectSpace (X,Y)) holds
( h = f + g iff for x being Element of X holds h . x = (f . x) + (g . x) ) by Th1;

theorem :: LOPBAN_1:12
for X being non empty set
for Y being RealLinearSpace
for f, h being VECTOR of (RealVectSpace (X,Y))
for a being Real holds
( h = a * f iff for x being Element of X holds h . x = a * (f . x) ) by Th2;

theorem :: LOPBAN_1:13
for X being non empty set
for Y being RealLinearSpace holds 0. (RealVectSpace (X,Y)) = X --> (0. Y) ;

begin

definition
let X, Y be non empty RLSStruct ;
let IT be Function of X,Y;
attrIT is homogeneous  means :Def5: :: LOPBAN_1:def 5
 for x being VECTOR of X
for r being Real holds IT . (r * x) = r * (IT . x);
end;

:: deftheorem Def5 defines homogeneous LOPBAN_1:def_5_:_
 for X, Y being non empty RLSStruct
for IT being Function of X,Y holds
( IT is homogeneous iff for x being VECTOR of X
for r being Real holds IT . (r * x) = r * (IT . x) );

registration
let X be non empty RLSStruct ;
let Y be RealLinearSpace;
cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous for Element of bool [: the carrier of X, the carrier of Y:];
existence
 ex b1 being Function of X,Y st
( b1 is additive & b1 is homogeneous )
proof
set f = the carrier of X --> (0. Y);
reconsider f = the carrier of X --> (0. Y) as Function of X,Y ;
take  f ; ::_thesis: ( f is additive & f is homogeneous )
hereby  :: according to VECTSP_1:def_20 ::_thesis: f is homogeneous
let x, y be VECTOR of X; ::_thesis: f . (x + y) = (f . x) + (f . y)
thus f . (x + y) = 0. Y by FUNCOP_1:7
.= (0. Y) + (0. Y) by RLVECT_1:4
.= (f . x) + (0. Y) by FUNCOP_1:7
.= (f . x) + (f . y) by FUNCOP_1:7 ; ::_thesis: verum
end;
hereby  :: according to LOPBAN_1:def_5 ::_thesis: verum
let x be VECTOR of X; ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; ::_thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = 0. Y by FUNCOP_1:7
.= r * (0. Y) by RLVECT_1:10
.= r * (f . x) by FUNCOP_1:7 ; ::_thesis: verum
end;
end;
end;

definition
let X, Y be RealLinearSpace;
mode LinearOperator of X,Y is additive homogeneous Function of X,Y;
end;

definition
let X, Y be RealLinearSpace;
func LinearOperators (X,Y) ->  Subset of (RealVectSpace ( the carrier of X,Y)) means :Def6: :: LOPBAN_1:def 6
 for x being set holds
( x in it iff x is LinearOperator of X,Y );
existence
 ex b1 being Subset of (RealVectSpace ( the carrier of X,Y)) st
for x being set holds
( x in b1 iff x is LinearOperator of X,Y )
proof
defpred S1[ set ] means $1 is LinearOperator of X,Y;
consider IT being set  such that
A1: for x being set holds
( x in IT iff ( x in Funcs ( the carrier of X, the carrier of Y) & S1[x] ) ) from XBOOLE_0:sch_1();
take  IT ; ::_thesis: ( IT is Subset of (RealVectSpace ( the carrier of X,Y)) & ( for x being set holds
( x in IT iff x is LinearOperator of X,Y ) ) )
 for x being set st x in IT holds
x in Funcs ( the carrier of X, the carrier of Y) by A1;
hence  IT is Subset of (RealVectSpace ( the carrier of X,Y)) by TARSKI:def_3; ::_thesis: for x being set holds
( x in IT iff x is LinearOperator of X,Y )
let x be set ; ::_thesis: ( x in IT iff x is LinearOperator of X,Y )
thus  ( x in IT implies x is LinearOperator of X,Y ) by A1; ::_thesis: ( x is LinearOperator of X,Y implies x in IT )
assume A2: x is LinearOperator of X,Y ; ::_thesis: x in IT
then  x in Funcs ( the carrier of X, the carrier of Y) by FUNCT_2:8;
hence  x in IT by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (RealVectSpace ( the carrier of X,Y)) st ( for x being set holds
( x in b1 iff x is LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is LinearOperator of X,Y ) ) holds
b1 = b2
proof
let X1, X2 be Subset of (RealVectSpace ( the carrier of X,Y)); ::_thesis: ( ( for x being set holds
( x in X1 iff x is LinearOperator of X,Y ) ) & ( for x being set holds
( x in X2 iff x is LinearOperator of X,Y ) ) implies X1 = X2 )
assume that
A3: for x being set holds
( x in X1 iff x is LinearOperator of X,Y ) and
A4: for x being set holds
( x in X2 iff x is LinearOperator of X,Y ) ; ::_thesis: X1 = X2
 for x being set st x in X2 holds
x in X1
proof
let x be set ; ::_thesis: ( x in X2 implies x in X1 )
assume  x in X2 ; ::_thesis: x in X1
then  x is LinearOperator of X,Y by A4;
hence  x in X1 by A3; ::_thesis: verum
end;
then A5: X2 c= X1 by TARSKI:def_3;
 for x being set st x in X1 holds
x in X2
proof
let x be set ; ::_thesis: ( x in X1 implies x in X2 )
assume  x in X1 ; ::_thesis: x in X2
then  x is LinearOperator of X,Y by A3;
hence  x in X2 by A4; ::_thesis: verum
end;
then  X1 c= X2 by TARSKI:def_3;
hence  X1 = X2 by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines LinearOperators LOPBAN_1:def_6_:_
 for X, Y being RealLinearSpace
for b3 being Subset of (RealVectSpace ( the carrier of X,Y)) holds
( b3 = LinearOperators (X,Y) iff for x being set holds
( x in b3 iff x is LinearOperator of X,Y ) );

registration
let X, Y be RealLinearSpace;
cluster LinearOperators (X,Y) ->  non empty functional ;
coherence
 ( not LinearOperators (X,Y) is empty & LinearOperators (X,Y) is functional )
proof
set f = the carrier of X --> (0. Y);
reconsider f = the carrier of X --> (0. Y) as Function of X,Y ;
A1: f is homogeneous
proof
let x be VECTOR of X; :: according to LOPBAN_1:def_5 ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; ::_thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = 0. Y by FUNCOP_1:7
.= r * (0. Y) by RLVECT_1:10
.= r * (f . x) by FUNCOP_1:7 ; ::_thesis: verum
end;
 f is additive
proof
let x, y be VECTOR of X; :: according to VECTSP_1:def_20 ::_thesis: f . (x + y) = (f . x) + (f . y)
thus f . (x + y) = 0. Y by FUNCOP_1:7
.= (0. Y) + (0. Y) by RLVECT_1:4
.= (f . x) + (0. Y) by FUNCOP_1:7
.= (f . x) + (f . y) by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  not LinearOperators (X,Y) is empty by A1, Def6; ::_thesis: LinearOperators (X,Y) is functional
let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in LinearOperators (X,Y) or x is set )
assume  x in LinearOperators (X,Y) ; ::_thesis: x is set
hence  x is set ; ::_thesis: verum
end;
end;

theorem Th14: :: LOPBAN_1:14
for X, Y being RealLinearSpace holds LinearOperators (X,Y) is linearly-closed
proof
let X, Y be RealLinearSpace; ::_thesis: LinearOperators (X,Y) is linearly-closed
set W = LinearOperators (X,Y);
A1: for v, u being VECTOR of (RealVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) & u in LinearOperators (X,Y) holds
v + u in LinearOperators (X,Y)
proof
let v, u be VECTOR of (RealVectSpace ( the carrier of X,Y)); ::_thesis: ( v in LinearOperators (X,Y) & u in LinearOperators (X,Y) implies v + u in LinearOperators (X,Y) )
assume that
A2: v in LinearOperators (X,Y) and
A3: u in LinearOperators (X,Y) ; ::_thesis: v + u in LinearOperators (X,Y)
 v + u is LinearOperator of X,Y
proof
reconsider f = v + u as Function of X,Y by FUNCT_2:66;
A4: f is homogeneous
proof
reconsider v9 = v, u9 = u as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x be VECTOR of X; :: according to LOPBAN_1:def_5 ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let s be Real; ::_thesis: f . (s * x) = s * (f . x)
A5: u9 is LinearOperator of X,Y by A3, Def6;
A6: v9 is LinearOperator of X,Y by A2, Def6;
thus f . (s * x) = (u9 . (s * x)) + (v9 . (s * x)) by Th1
.= (s * (u9 . x)) + (v9 . (s * x)) by A5, Def5
.= (s * (u9 . x)) + (s * (v9 . x)) by A6, Def5
.= s * ((u9 . x) + (v9 . x)) by RLVECT_1:def_5
.= s * (f . x) by Th1 ; ::_thesis: verum
end;
 f is additive
proof
reconsider v9 = v, u9 = u as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x, y be VECTOR of X; :: according to VECTSP_1:def_20 ::_thesis: f . (x + y) = (f . x) + (f . y)
A7: u9 is LinearOperator of X,Y by A3, Def6;
A8: v9 is LinearOperator of X,Y by A2, Def6;
thus f . (x + y) = (u9 . (x + y)) + (v9 . (x + y)) by Th1
.= ((u9 . x) + (u9 . y)) + (v9 . (x + y)) by A7, VECTSP_1:def_20
.= ((u9 . x) + (u9 . y)) + ((v9 . x) + (v9 . y)) by A8, VECTSP_1:def_20
.= (((u9 . x) + (u9 . y)) + (v9 . x)) + (v9 . y) by RLVECT_1:def_3
.= (((u9 . x) + (v9 . x)) + (u9 . y)) + (v9 . y) by RLVECT_1:def_3
.= ((f . x) + (u9 . y)) + (v9 . y) by Th1
.= (f . x) + ((u9 . y) + (v9 . y)) by RLVECT_1:def_3
.= (f . x) + (f . y) by Th1 ; ::_thesis: verum
end;
hence  v + u is LinearOperator of X,Y by A4; ::_thesis: verum
end;
hence  v + u in LinearOperators (X,Y) by Def6; ::_thesis: verum
end;
 for a being Real
for v being VECTOR of (RealVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds
a * v in LinearOperators (X,Y)
proof
let a be Real; ::_thesis: for v being VECTOR of (RealVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds
a * v in LinearOperators (X,Y)
let v be VECTOR of (RealVectSpace ( the carrier of X,Y)); ::_thesis: ( v in LinearOperators (X,Y) implies a * v in LinearOperators (X,Y) )
assume A9: v in LinearOperators (X,Y) ; ::_thesis: a * v in LinearOperators (X,Y)
 a * v is LinearOperator of X,Y
proof
reconsider f = a * v as Function of X,Y by FUNCT_2:66;
A10: f is homogeneous
proof
reconsider v9 = v as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x be VECTOR of X; :: according to LOPBAN_1:def_5 ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let s be Real; ::_thesis: f . (s * x) = s * (f . x)
A11: v9 is LinearOperator of X,Y by A9, Def6;
thus f . (s * x) = a * (v9 . (s * x)) by Th2
.= a * (s * (v9 . x)) by A11, Def5
.= (a * s) * (v9 . x) by RLVECT_1:def_7
.= s * (a * (v9 . x)) by RLVECT_1:def_7
.= s * (f . x) by Th2 ; ::_thesis: verum
end;
 f is additive
proof
reconsider v9 = v as Element of Funcs ( the carrier of X, the carrier of Y) ;
let x, y be VECTOR of X; :: according to VECTSP_1:def_20 ::_thesis: f . (x + y) = (f . x) + (f . y)
A12: v9 is LinearOperator of X,Y by A9, Def6;
thus f . (x + y) = a * (v9 . (x + y)) by Th2
.= a * ((v9 . x) + (v9 . y)) by A12, VECTSP_1:def_20
.= (a * (v9 . x)) + (a * (v9 . y)) by RLVECT_1:def_5
.= (f . x) + (a * (v9 . y)) by Th2
.= (f . x) + (f . y) by Th2 ; ::_thesis: verum
end;
hence  a * v is LinearOperator of X,Y by A10; ::_thesis: verum
end;
hence  a * v in LinearOperators (X,Y) by Def6; ::_thesis: verum
end;
hence  LinearOperators (X,Y) is linearly-closed by A1, RLSUB_1:def_1; ::_thesis: verum
end;

theorem :: LOPBAN_1:15
for X, Y being RealLinearSpace holds RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Subspace of RealVectSpace ( the carrier of X,Y) by Th14, RSSPACE:11;

registration
let X, Y be RealLinearSpace;
cluster RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Abelian & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is add-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_zeroed & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_complementable & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is vector-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-unital ) by Th14, RSSPACE:11;
end;

definition
let X, Y be RealLinearSpace;
func R_VectorSpace_of_LinearOperators (X,Y) ->  RealLinearSpace equals :: LOPBAN_1:def 7
 RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);
coherence
 RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is RealLinearSpace ;
end;

:: deftheorem  defines R_VectorSpace_of_LinearOperators LOPBAN_1:def_7_:_
 for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators (X,Y) = RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);

registration
let X, Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators (X,Y) ->  strict ;
coherence
 R_VectorSpace_of_LinearOperators (X,Y) is strict ;
end;

registration
let X, Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators (X,Y) ->  constituted-Functions ;
coherence
 R_VectorSpace_of_LinearOperators (X,Y) is constituted-Functions by MONOID_0:80;
end;

definition
let X, Y be RealLinearSpace;
let f be Element of (R_VectorSpace_of_LinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine funcf . v ->  VECTOR of Y;
coherence
 f . v is VECTOR of Y
proof
reconsider f = f as LinearOperator of X,Y by Def6;
 f . v is VECTOR of Y ;
hence  f . v is VECTOR of Y ; ::_thesis: verum
end;
end;

theorem Th16: :: LOPBAN_1:16
for X, Y being RealLinearSpace
for f, g, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof
let X, Y be RealLinearSpace; ::_thesis: for f, g, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
let f, g, h be VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)); ::_thesis: ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
reconsider f9 = f, g9 = g, h9 = h as LinearOperator of X,Y by Def6;
A1: R_VectorSpace_of_LinearOperators (X,Y) is Subspace of RealVectSpace ( the carrier of X,Y) by Th14, RSSPACE:11;
then reconsider f1 = f as VECTOR of (RealVectSpace ( the carrier of X,Y)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (RealVectSpace ( the carrier of X,Y)) by A1, RLSUB_1:10;
reconsider g1 = g as VECTOR of (RealVectSpace ( the carrier of X,Y)) by A1, RLSUB_1:10;
A2: now__::_thesis:_(_h_=_f_+_g_implies_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_)
assume A3: h = f + g ; ::_thesis: for x being Element of X holds h9 . x = (f9 . x) + (g9 . x)
let x be Element of X; ::_thesis: h9 . x = (f9 . x) + (g9 . x)
 h1 = f1 + g1 by A1, A3, RLSUB_1:13;
hence  h9 . x = (f9 . x) + (g9 . x) by Th1; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_(f9_._x)_+_(g9_._x)_)_implies_h_=_f_+_g_)
assume  for x being Element of X holds h9 . x = (f9 . x) + (g9 . x) ; ::_thesis: h = f + g
then  h1 = f1 + g1 by Th1;
hence  h = f + g by A1, RLSUB_1:13; ::_thesis: verum
end;
hence  ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) ) by A2; ::_thesis: verum
end;

theorem Th17: :: LOPBAN_1:17
for X, Y being RealLinearSpace
for f, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof
let X, Y be RealLinearSpace; ::_thesis: for f, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
let f, h be VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)); ::_thesis: for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
reconsider f9 = f, h9 = h as LinearOperator of X,Y by Def6;
let a be Real; ::_thesis: ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
A1: R_VectorSpace_of_LinearOperators (X,Y) is Subspace of RealVectSpace ( the carrier of X,Y) by Th14, RSSPACE:11;
then reconsider f1 = f as VECTOR of (RealVectSpace ( the carrier of X,Y)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (RealVectSpace ( the carrier of X,Y)) by A1, RLSUB_1:10;
A2: now__::_thesis:_(_h_=_a_*_f_implies_for_x_being_Element_of_X_holds_h9_._x_=_a_*_(f9_._x)_)
assume A3: h = a * f ; ::_thesis: for x being Element of X holds h9 . x = a * (f9 . x)
let x be Element of X; ::_thesis: h9 . x = a * (f9 . x)
 h1 = a * f1 by A1, A3, RLSUB_1:14;
hence  h9 . x = a * (f9 . x) by Th2; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_a_*_(f9_._x)_)_implies_h_=_a_*_f_)
assume  for x being Element of X holds h9 . x = a * (f9 . x) ; ::_thesis: h = a * f
then  h1 = a * f1 by Th2;
hence  h = a * f by A1, RLSUB_1:14; ::_thesis: verum
end;
hence  ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) ) by A2; ::_thesis: verum
end;

theorem Th18: :: LOPBAN_1:18
for X, Y being RealLinearSpace holds 0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)
proof
let X, Y be RealLinearSpace; ::_thesis: 0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)
A1: 0. (RealVectSpace ( the carrier of X,Y)) = the carrier of X --> (0. Y) ;
 R_VectorSpace_of_LinearOperators (X,Y) is Subspace of RealVectSpace ( the carrier of X,Y) by Th14, RSSPACE:11;
hence  0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, RLSUB_1:11; ::_thesis: verum
end;

theorem Th19: :: LOPBAN_1:19
for X, Y being RealLinearSpace holds the carrier of X --> (0. Y) is LinearOperator of X,Y
proof
let X, Y be RealLinearSpace; ::_thesis: the carrier of X --> (0. Y) is LinearOperator of X,Y
set f = the carrier of X --> (0. Y);
reconsider f = the carrier of X --> (0. Y) as Function of X,Y ;
A1: f is homogeneous
proof
let x be VECTOR of X; :: according to LOPBAN_1:def_5 ::_thesis: for r being Real holds f . (r * x) = r * (f . x)
let r be Real; ::_thesis: f . (r * x) = r * (f . x)
thus f . (r * x) = 0. Y by FUNCOP_1:7
.= r * (0. Y) by RLVECT_1:10
.= r * (f . x) by FUNCOP_1:7 ; ::_thesis: verum
end;
 f is additive
proof
let x, y be VECTOR of X; :: according to VECTSP_1:def_20 ::_thesis: f . (x + y) = (f . x) + (f . y)
thus f . (x + y) = 0. Y by FUNCOP_1:7
.= (0. Y) + (0. Y) by RLVECT_1:4
.= (f . x) + (0. Y) by FUNCOP_1:7
.= (f . x) + (f . y) by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  the carrier of X --> (0. Y) is LinearOperator of X,Y by A1; ::_thesis: verum
end;

begin

theorem Th20: :: LOPBAN_1:20
for X being RealNormSpace
for seq being sequence of X
for g being Point of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for g being Point of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
let seq be sequence of X; ::_thesis: for g being Point of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
let g be Point of X; ::_thesis: ( seq is convergent & lim seq = g implies ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; ::_thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
A3: now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_k_<=_n_holds_
abs_((||.seq.||_._n)_-_||.g.||)_<_r
let r be real number ; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r )
assume A4: r > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r
 r is Real by XREAL_0:def_1;
then consider m1 being Element of NAT  such that
A5: for n being Element of NAT st n >= m1 holds
||.((seq . n) - g).|| < r by A1, A2, A4, NORMSP_1:def_7;
take k = m1; ::_thesis: for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
abs_((||.seq.||_._n)_-_||.g.||)_<_r
let n be Element of NAT ; ::_thesis: ( n >= k implies abs ((||.seq.|| . n) - ||.g.||) < r )
assume  n >= k ; ::_thesis: abs ((||.seq.|| . n) - ||.g.||) < r
then A6: ||.((seq . n) - g).|| < r by A5;
 abs (||.(seq . n).|| - ||.g.||) <= ||.((seq . n) - g).|| by NORMSP_1:9;
then  abs (||.(seq . n).|| - ||.g.||) < r by A6, XXREAL_0:2;
hence  abs ((||.seq.|| . n) - ||.g.||) < r by NORMSP_0:def_4; ::_thesis: verum
end;
hence  for n being Element of NAT st k <= n holds
abs ((||.seq.|| . n) - ||.g.||) < r ; ::_thesis: verum
end;
 ||.seq.|| is convergent by A1, NORMSP_1:23;
hence  ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| ) by A3, SEQ_2:def_7; ::_thesis: verum
end;

definition
let X, Y be RealNormSpace;
let IT be LinearOperator of X,Y;
attrIT is Lipschitzian  means :Def8: :: LOPBAN_1:def 8
 ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) );
end;

:: deftheorem Def8 defines Lipschitzian LOPBAN_1:def_8_:_
 for X, Y being RealNormSpace
for IT being LinearOperator of X,Y holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) ) );

theorem Th21: :: LOPBAN_1:21
for X, Y being RealNormSpace
for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds
f is Lipschitzian
proof
let X, Y be RealNormSpace; ::_thesis: for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds
f is Lipschitzian
let f be LinearOperator of X,Y; ::_thesis: ( ( for x being VECTOR of X holds f . x = 0. Y ) implies f is Lipschitzian )
assume A1: for x being VECTOR of X holds f . x = 0. Y ; ::_thesis: f is Lipschitzian
A2: now__::_thesis:_for_x_being_VECTOR_of_X_holds_||.(f_._x).||_=_0_*_||.x.||
let x be VECTOR of X; ::_thesis: ||.(f . x).|| = 0 * ||.x.||
thus ||.(f . x).|| = ||.(0. Y).|| by A1
.= 0 * ||.x.|| ; ::_thesis: verum
end;
take  0 ; :: according to LOPBAN_1:def_8 ::_thesis: ( 0 <= 0 & ( for x being VECTOR of X holds ||.(f . x).|| <= 0 * ||.x.|| ) )
thus  ( 0 <= 0 & ( for x being VECTOR of X holds ||.(f . x).|| <= 0 * ||.x.|| ) ) by A2; ::_thesis: verum
end;

registration
let X, Y be RealNormSpace;
cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous Lipschitzian for Element of bool [: the carrier of X, the carrier of Y:];
existence
 ex b1 being LinearOperator of X,Y st b1 is Lipschitzian
proof
set f = the carrier of X --> (0. Y);
reconsider f = the carrier of X --> (0. Y) as LinearOperator of X,Y by Th19;
take  f ; ::_thesis: f is Lipschitzian
 for x being VECTOR of X holds f . x = 0. Y by FUNCOP_1:7;
hence  f is Lipschitzian by Th21; ::_thesis: verum
end;
end;

definition
let X, Y be RealNormSpace;
func BoundedLinearOperators (X,Y) ->  Subset of (R_VectorSpace_of_LinearOperators (X,Y)) means :Def9: :: LOPBAN_1:def 9
 for x being set holds
( x in it iff x is Lipschitzian LinearOperator of X,Y );
existence
 ex b1 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st
for x being set holds
( x in b1 iff x is Lipschitzian LinearOperator of X,Y )
proof
defpred S1[ set ] means $1 is Lipschitzian LinearOperator of X,Y;
consider IT being set  such that
A1: for x being set holds
( x in IT iff ( x in LinearOperators (X,Y) & S1[x] ) ) from XBOOLE_0:sch_1();
take  IT ; ::_thesis: ( IT is Subset of (R_VectorSpace_of_LinearOperators (X,Y)) & ( for x being set holds
( x in IT iff x is Lipschitzian LinearOperator of X,Y ) ) )
 for x being set st x in IT holds
x in LinearOperators (X,Y) by A1;
hence  IT is Subset of (R_VectorSpace_of_LinearOperators (X,Y)) by TARSKI:def_3; ::_thesis: for x being set holds
( x in IT iff x is Lipschitzian LinearOperator of X,Y )
let x be set ; ::_thesis: ( x in IT iff x is Lipschitzian LinearOperator of X,Y )
thus  ( x in IT implies x is Lipschitzian LinearOperator of X,Y ) by A1; ::_thesis: ( x is Lipschitzian LinearOperator of X,Y implies x in IT )
assume A2: x is Lipschitzian LinearOperator of X,Y ; ::_thesis: x in IT
then  x in LinearOperators (X,Y) by Def6;
hence  x in IT by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st ( for x being set holds
( x in b1 iff x is Lipschitzian LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is Lipschitzian LinearOperator of X,Y ) ) holds
b1 = b2
proof
let X1, X2 be Subset of (R_VectorSpace_of_LinearOperators (X,Y)); ::_thesis: ( ( for x being set holds
( x in X1 iff x is Lipschitzian LinearOperator of X,Y ) ) & ( for x being set holds
( x in X2 iff x is Lipschitzian LinearOperator of X,Y ) ) implies X1 = X2 )
assume that
A3: for x being set holds
( x in X1 iff x is Lipschitzian LinearOperator of X,Y ) and
A4: for x being set holds
( x in X2 iff x is Lipschitzian LinearOperator of X,Y ) ; ::_thesis: X1 = X2
 for x being set st x in X2 holds
x in X1
proof
let x be set ; ::_thesis: ( x in X2 implies x in X1 )
assume  x in X2 ; ::_thesis: x in X1
then  x is Lipschitzian LinearOperator of X,Y by A4;
hence  x in X1 by A3; ::_thesis: verum
end;
then A5: X2 c= X1 by TARSKI:def_3;
 for x being set st x in X1 holds
x in X2
proof
let x be set ; ::_thesis: ( x in X1 implies x in X2 )
assume  x in X1 ; ::_thesis: x in X2
then  x is Lipschitzian LinearOperator of X,Y by A3;
hence  x in X2 by A4; ::_thesis: verum
end;
then  X1 c= X2 by TARSKI:def_3;
hence  X1 = X2 by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines BoundedLinearOperators LOPBAN_1:def_9_:_
 for X, Y being RealNormSpace
for b3 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) holds
( b3 = BoundedLinearOperators (X,Y) iff for x being set holds
( x in b3 iff x is Lipschitzian LinearOperator of X,Y ) );

registration
let X, Y be RealNormSpace;
cluster BoundedLinearOperators (X,Y) ->  non empty ;
coherence
 not BoundedLinearOperators (X,Y) is empty
proof
set f = the carrier of X --> (0. Y);
reconsider f = the carrier of X --> (0. Y) as LinearOperator of X,Y by Th19;
 for x being VECTOR of X holds f . x = 0. Y by FUNCOP_1:7;
then  f is Lipschitzian by Th21;
hence  not BoundedLinearOperators (X,Y) is empty by Def9; ::_thesis: verum
end;
end;

theorem Th22: :: LOPBAN_1:22
for X, Y being RealNormSpace holds BoundedLinearOperators (X,Y) is linearly-closed
proof
let X, Y be RealNormSpace; ::_thesis: BoundedLinearOperators (X,Y) is linearly-closed
set W = BoundedLinearOperators (X,Y);
A1: for v, u being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) & u in BoundedLinearOperators (X,Y) holds
v + u in BoundedLinearOperators (X,Y)
proof
let v, u be VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)); ::_thesis: ( v in BoundedLinearOperators (X,Y) & u in BoundedLinearOperators (X,Y) implies v + u in BoundedLinearOperators (X,Y) )
assume that
A2: v in BoundedLinearOperators (X,Y) and
A3: u in BoundedLinearOperators (X,Y) ; ::_thesis: v + u in BoundedLinearOperators (X,Y)
reconsider f = v + u as LinearOperator of X,Y by Def6;
 f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by A2, Def9;
consider K2 being Real such that
A4: 0 <= K2 and
A5: for x being VECTOR of X holds ||.(v1 . x).|| <= K2 * ||.x.|| by Def8;
reconsider u1 = u as Lipschitzian LinearOperator of X,Y by A3, Def9;
consider K1 being Real such that
A6: 0 <= K1 and
A7: for x being VECTOR of X holds ||.(u1 . x).|| <= K1 * ||.x.|| by Def8;
take K3 = K1 + K2; :: according to LOPBAN_1:def_8 ::_thesis: ( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ||.x.|| ) )
now__::_thesis:_for_x_being_VECTOR_of_X_holds_||.(f_._x).||_<=_K3_*_||.x.||
let x be VECTOR of X; ::_thesis: ||.(f . x).|| <= K3 * ||.x.||
A8: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by NORMSP_1:def_1;
A9: ||.(v1 . x).|| <= K2 * ||.x.|| by A5;
 ||.(u1 . x).|| <= K1 * ||.x.|| by A7;
then A10: ||.(u1 . x).|| + ||.(v1 . x).|| <= (K1 * ||.x.||) + (K2 * ||.x.||) by A9, XREAL_1:7;
 ||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th16;
hence  ||.(f . x).|| <= K3 * ||.x.|| by A8, A10, XXREAL_0:2; ::_thesis: verum
end;
hence  ( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ||.x.|| ) ) by A6, A4; ::_thesis: verum
end;
hence  v + u in BoundedLinearOperators (X,Y) by Def9; ::_thesis: verum
end;
 for a being Real
for v being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) holds
a * v in BoundedLinearOperators (X,Y)
proof
let a be Real; ::_thesis: for v being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) holds
a * v in BoundedLinearOperators (X,Y)
let v be VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)); ::_thesis: ( v in BoundedLinearOperators (X,Y) implies a * v in BoundedLinearOperators (X,Y) )
assume A11: v in BoundedLinearOperators (X,Y) ; ::_thesis: a * v in BoundedLinearOperators (X,Y)
reconsider f = a * v as LinearOperator of X,Y by Def6;
 f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by A11, Def9;
consider K being Real such that
A12: 0 <= K and
A13: for x being VECTOR of X holds ||.(v1 . x).|| <= K * ||.x.|| by Def8;
take  (abs a) * K ; :: according to LOPBAN_1:def_8 ::_thesis: ( 0 <= (abs a) * K & ( for x being VECTOR of X holds ||.(f . x).|| <= ((abs a) * K) * ||.x.|| ) )
A14: now__::_thesis:_for_x_being_VECTOR_of_X_holds_||.(f_._x).||_<=_((abs_a)_*_K)_*_||.x.||
let x be VECTOR of X; ::_thesis: ||.(f . x).|| <= ((abs a) * K) * ||.x.||
 0 <= abs a by COMPLEX1:46;
then A15: (abs a) * ||.(v1 . x).|| <= (abs a) * (K * ||.x.||) by A13, XREAL_1:64;
 ||.(a * (v1 . x)).|| = (abs a) * ||.(v1 . x).|| by NORMSP_1:def_1;
hence  ||.(f . x).|| <= ((abs a) * K) * ||.x.|| by A15, Th17; ::_thesis: verum
end;
 0 <= abs a by COMPLEX1:46;
hence  ( 0 <= (abs a) * K & ( for x being VECTOR of X holds ||.(f . x).|| <= ((abs a) * K) * ||.x.|| ) ) by A12, A14; ::_thesis: verum
end;
hence  a * v in BoundedLinearOperators (X,Y) by Def9; ::_thesis: verum
end;
hence  BoundedLinearOperators (X,Y) is linearly-closed by A1, RLSUB_1:def_1; ::_thesis: verum
end;

theorem :: LOPBAN_1:23
for X, Y being RealNormSpace holds RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Subspace of R_VectorSpace_of_LinearOperators (X,Y) by Th22, RSSPACE:11;

registration
let X, Y be RealNormSpace;
cluster RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital ) by Th22, RSSPACE:11;
end;

definition
let X, Y be RealNormSpace;
func R_VectorSpace_of_BoundedLinearOperators (X,Y) ->  RealLinearSpace equals :: LOPBAN_1:def 10
 RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);
coherence
 RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace ;
end;

:: deftheorem  defines R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def_10_:_
 for X, Y being RealNormSpace holds R_VectorSpace_of_BoundedLinearOperators (X,Y) = RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);

registration
let X, Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedLinearOperators (X,Y) ->  strict ;
coherence
 R_VectorSpace_of_BoundedLinearOperators (X,Y) is strict ;
end;

registration
let X, Y be RealNormSpace;
cluster  ->  Relation-like Function-like for Element of the carrier of (R_VectorSpace_of_BoundedLinearOperators (X,Y));
coherence
 for b1 being Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds
( b1 is Function-like & b1 is Relation-like ) ;
end;

definition
let X, Y be RealNormSpace;
let f be Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine funcf . v ->  VECTOR of Y;
coherence
 f . v is VECTOR of Y
proof
reconsider f = f as LinearOperator of X,Y by Def9;
 f . v is VECTOR of Y ;
hence  f . v is VECTOR of Y ; ::_thesis: verum
end;
end;

theorem Th24: :: LOPBAN_1:24
for X, Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof
let X, Y be RealNormSpace; ::_thesis: for f, g, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
let f, g, h be VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
A1: R_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of R_VectorSpace_of_LinearOperators (X,Y) by Th22, RSSPACE:11;
then reconsider f1 = f as VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) by A1, RLSUB_1:10;
reconsider g1 = g as VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) by A1, RLSUB_1:10;
hereby  ::_thesis: ( ( for x being VECTOR of X holds h . x = (f . x) + (g . x) ) implies h = f + g )
assume A2: h = f + g ; ::_thesis: for x being Element of X holds h . x = (f . x) + (g . x)
let x be Element of X; ::_thesis: h . x = (f . x) + (g . x)
 h1 = f1 + g1 by A1, A2, RLSUB_1:13;
hence  h . x = (f . x) + (g . x) by Th16; ::_thesis: verum
end;
assume  for x being Element of X holds h . x = (f . x) + (g . x) ; ::_thesis: h = f + g
then  h1 = f1 + g1 by Th16;
hence  h = f + g by A1, RLSUB_1:13; ::_thesis: verum
end;

theorem Th25: :: LOPBAN_1:25
for X, Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof
let X, Y be RealNormSpace; ::_thesis: for f, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
let f, h be VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
let a be Real; ::_thesis: ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
A1: R_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of R_VectorSpace_of_LinearOperators (X,Y) by Th22, RSSPACE:11;
then reconsider f1 = f as VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) by A1, RLSUB_1:10;
hereby  ::_thesis: ( ( for x being VECTOR of X holds h . x = a * (f . x) ) implies h = a * f )
assume A2: h = a * f ; ::_thesis: for x being Element of X holds h . x = a * (f . x)
let x be Element of X; ::_thesis: h . x = a * (f . x)
 h1 = a * f1 by A1, A2, RLSUB_1:14;
hence  h . x = a * (f . x) by Th17; ::_thesis: verum
end;
assume  for x being Element of X holds h . x = a * (f . x) ; ::_thesis: h = a * f
then  h1 = a * f1 by Th17;
hence  h = a * f by A1, RLSUB_1:14; ::_thesis: verum
end;

theorem Th26: :: LOPBAN_1:26
for X, Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y)
proof
let X, Y be RealNormSpace; ::_thesis: 0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y)
A1: 0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) by Th18;
 R_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of R_VectorSpace_of_LinearOperators (X,Y) by Th22, RSSPACE:11;
hence  0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, RLSUB_1:11; ::_thesis: verum
end;

definition
let X, Y be RealNormSpace;
let f be set ;
assume A1: f in BoundedLinearOperators (X,Y) ;
func modetrans (f,X,Y) ->  Lipschitzian LinearOperator of X,Y equals :Def11: :: LOPBAN_1:def 11
f;
coherence
 f is Lipschitzian LinearOperator of X,Y by A1, Def9;
end;

:: deftheorem Def11 defines modetrans LOPBAN_1:def_11_:_
 for X, Y being RealNormSpace
for f being set st f in BoundedLinearOperators (X,Y) holds
modetrans (f,X,Y) = f;

definition
let X, Y be RealNormSpace;
let u be LinearOperator of X,Y;
func PreNorms u ->  non empty Subset of REAL equals :: LOPBAN_1:def 12
 {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  ;
coherence
  {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  is non empty Subset of REAL
proof
A1: now__::_thesis:_for_x_being_set_st_x_in__{__||.(u_._t).||_where_t_is_VECTOR_of_X_:_||.t.||_<=_1__}__holds_
x_in_REAL
let x be set ; ::_thesis: ( x in  {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  implies x in REAL )
now__::_thesis:_(_x_in__{__||.(u_._t).||_where_t_is_VECTOR_of_X_:_||.t.||_<=_1__}__implies_x_in_REAL_)
assume  x in  {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  ; ::_thesis: x in REAL
then  ex t being VECTOR of X st
( x = ||.(u . t).|| & ||.t.|| <= 1 ) ;
hence  x in REAL ; ::_thesis: verum
end;
hence  ( x in  {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  implies x in REAL ) ; ::_thesis: verum
end;
 ||.(0. X).|| = 0 ;
then  ||.(u . (0. X)).|| in  {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  ;
hence   {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  is non empty Subset of REAL by A1, TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines PreNorms LOPBAN_1:def_12_:_
 for X, Y being RealNormSpace
for u being LinearOperator of X,Y holds PreNorms u =  {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  ;

theorem Th27: :: LOPBAN_1:27
for X, Y being RealNormSpace
for g being Lipschitzian LinearOperator of X,Y holds PreNorms g is bounded_above
proof
let X, Y be RealNormSpace; ::_thesis: for g being Lipschitzian LinearOperator of X,Y holds PreNorms g is bounded_above
let g be Lipschitzian LinearOperator of X,Y; ::_thesis: PreNorms g is bounded_above
 PreNorms g is bounded_above
proof
consider K being Real such that
A1: 0 <= K and
A2: for x being VECTOR of X holds ||.(g . x).|| <= K * ||.x.|| by Def8;
take  K ; :: according to XXREAL_2:def_10 ::_thesis: K is UpperBound of PreNorms g
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in PreNorms g or r <= K )
assume  r in PreNorms g ; ::_thesis: r <= K
then consider t being VECTOR of X such that
A3: r = ||.(g . t).|| and
A4: ||.t.|| <= 1 ;
A5: ||.(g . t).|| <= K * ||.t.|| by A2;
 K * ||.t.|| <= K * 1 by A1, A4, XREAL_1:64;
hence  r <= K by A3, A5, XXREAL_0:2; ::_thesis: verum
end;
hence  PreNorms g is bounded_above ; ::_thesis: verum
end;

theorem :: LOPBAN_1:28
for X, Y being RealNormSpace
for g being LinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )
proof
let X, Y be RealNormSpace; ::_thesis: for g being LinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )
let g be LinearOperator of X,Y; ::_thesis: ( g is Lipschitzian iff PreNorms g is bounded_above )
now__::_thesis:_(_PreNorms_g_is_bounded_above_implies_ex_K_being_Real_st_g_is_Lipschitzian_)
reconsider K = upper_bound (PreNorms g) as Real ;
assume A1: PreNorms g is bounded_above ; ::_thesis: ex K being Real st g is Lipschitzian
A2: now__::_thesis:_for_t_being_VECTOR_of_X_holds_||.(g_._t).||_<=_K_*_||.t.||
let t be VECTOR of X; ::_thesis: ||.(g . t).|| <= K * ||.t.||
now__::_thesis:_(_(_t_=_0._X_&_||.(g_._t).||_<=_K_*_||.t.||_)_or_(_t_<>_0._X_&_||.(g_._t).||_<=_K_*_||.t.||_)_)
percases ( t = 0. X or t <> 0. X ) ;
caseA3: t = 0. X ; ::_thesis: ||.(g . t).|| <= K * ||.t.||
then A4: ||.t.|| = 0 ;
g . t = g . (0 * (0. X)) by A3, RLVECT_1:10
.= 0 * (g . (0. X)) by Def5
.= 0. Y by RLVECT_1:10 ;
hence  ||.(g . t).|| <= K * ||.t.|| by A4; ::_thesis: verum
end;
caseA5: t <> 0. X ; ::_thesis: ||.(g . t).|| <= K * ||.t.||
reconsider t1 = (||.t.|| ") * t as VECTOR of X ;
A6: ||.t.|| <> 0 by A5, NORMSP_0:def_5;
A7: (||.(g . t).|| / ||.t.||) * ||.t.|| = (||.(g . t).|| * (||.t.|| ")) * ||.t.|| by XCMPLX_0:def_9
.= ||.(g . t).|| * ((||.t.|| ") * ||.t.||)
.= ||.(g . t).|| * 1 by A6, XCMPLX_0:def_7
.= ||.(g . t).|| ;
A8: abs (||.t.|| ") = abs (1 * (||.t.|| "))
.= abs (1 / ||.t.||) by XCMPLX_0:def_9
.= 1 / (abs ||.t.||) by ABSVALUE:7
.= 1 / ||.t.|| by ABSVALUE:def_1
.= 1 * (||.t.|| ") by XCMPLX_0:def_9
.= ||.t.|| " ;
||.t1.|| = (abs (||.t.|| ")) * ||.t.|| by NORMSP_1:def_1
.= 1 by A6, A8, XCMPLX_0:def_7 ;
then A9: ||.(g . t1).|| in  {  ||.(g . s).|| where s is VECTOR of X : ||.s.|| <= 1  }  ;
||.(g . t).|| / ||.t.|| = ||.(g . t).|| * (||.t.|| ") by XCMPLX_0:def_9
.= ||.((||.t.|| ") * (g . t)).|| by A8, NORMSP_1:def_1
.= ||.(g . t1).|| by Def5 ;
then  ||.(g . t).|| / ||.t.|| <= K by A1, A9, SEQ_4:def_1;
hence  ||.(g . t).|| <= K * ||.t.|| by A7, XREAL_1:64; ::_thesis: verum
end;
end;
end;
hence  ||.(g . t).|| <= K * ||.t.|| ; ::_thesis: verum
end;
take K = K; ::_thesis: g is Lipschitzian
 0 <= K
proof
consider r0 being set  such that
A10: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A10;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume  r in PreNorms g ; ::_thesis: 0 <= r
then  ex t being VECTOR of X st
( r = ||.(g . t).|| & ||.t.|| <= 1 ) ;
hence  0 <= r ; ::_thesis: verum
end;
then  0 <= r0 by A10;
hence  0 <= K by A1, A10, SEQ_4:def_1; ::_thesis: verum
end;
hence  g is Lipschitzian by A2, Def8; ::_thesis: verum
end;
hence  ( g is Lipschitzian iff PreNorms g is bounded_above ) by Th27; ::_thesis: verum
end;

definition
let X, Y be RealNormSpace;
func BoundedLinearOperatorsNorm (X,Y) ->  Function of (BoundedLinearOperators (X,Y)),REAL means :Def13: :: LOPBAN_1:def 13
 for x being set st x in BoundedLinearOperators (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));
existence
 ex b1 being Function of (BoundedLinearOperators (X,Y)),REAL st
for x being set st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
proof
deffunc H1( set ) ->  Element of REAL = upper_bound (PreNorms (modetrans ($1,X,Y)));
A1: for z being set st z in BoundedLinearOperators (X,Y) holds
H1(z) in REAL ;
thus  ex f being Function of (BoundedLinearOperators (X,Y)),REAL st
for x being set st x in BoundedLinearOperators (X,Y) holds
f . x = H1(x) from FUNCT_2:sch_2(A1); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (BoundedLinearOperators (X,Y)),REAL st ( for x being set st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedLinearOperators (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of (BoundedLinearOperators (X,Y)),REAL; ::_thesis: ( ( for x being set st x in BoundedLinearOperators (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedLinearOperators (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in BoundedLinearOperators (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) and
A3: for x being set st x in BoundedLinearOperators (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in BoundedLinearOperators (X,Y) holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in BoundedLinearOperators (X,Y) implies NORM1 . z = NORM2 . z )
assume A5: z in BoundedLinearOperators (X,Y) ; ::_thesis: NORM1 . z = NORM2 . z
 NORM1 . z = upper_bound (PreNorms (modetrans (z,X,Y))) by A2, A5;
hence  NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
A6: dom NORM2 = BoundedLinearOperators (X,Y) by FUNCT_2:def_1;
 dom NORM1 = BoundedLinearOperators (X,Y) by FUNCT_2:def_1;
hence  NORM1 = NORM2 by A6, A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines BoundedLinearOperatorsNorm LOPBAN_1:def_13_:_
 for X, Y being RealNormSpace
for b3 being Function of (BoundedLinearOperators (X,Y)),REAL holds
( b3 = BoundedLinearOperatorsNorm (X,Y) iff for x being set st x in BoundedLinearOperators (X,Y) holds
b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) );

theorem Th29: :: LOPBAN_1:29
for X, Y being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y holds modetrans (f,X,Y) = f
proof
let X, Y be RealNormSpace; ::_thesis: for f being Lipschitzian LinearOperator of X,Y holds modetrans (f,X,Y) = f
let f be Lipschitzian LinearOperator of X,Y; ::_thesis: modetrans (f,X,Y) = f
 f in BoundedLinearOperators (X,Y) by Def9;
hence  modetrans (f,X,Y) = f by Def11; ::_thesis: verum
end;

theorem Th30: :: LOPBAN_1:30
for X, Y being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
proof
let X, Y be RealNormSpace; ::_thesis: for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
let f be Lipschitzian LinearOperator of X,Y; ::_thesis: (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
reconsider f9 = f as set ;
 f in BoundedLinearOperators (X,Y) by Def9;
hence (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def13
.= upper_bound (PreNorms f) by Th29 ;
::_thesis: verum
end;

definition
let X, Y be RealNormSpace;
func R_NormSpace_of_BoundedLinearOperators (X,Y) ->  non empty NORMSTR  equals :: LOPBAN_1:def 14
 NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);
coherence
 NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty NORMSTR ;
end;

:: deftheorem  defines R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def_14_:_
 for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) = NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);

theorem Th31: :: LOPBAN_1:31
for X, Y being RealNormSpace holds the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y))
proof
let X, Y be RealNormSpace; ::_thesis: the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y))
the carrier of X --> (0. Y) = 0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) by Th26
.= 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
hence  the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ; ::_thesis: verum
end;

theorem Th32: :: LOPBAN_1:32
for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being Lipschitzian LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
proof
let X, Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being Lipschitzian LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for g being Lipschitzian LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
let g be Lipschitzian LinearOperator of X,Y; ::_thesis: ( g = f implies for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.|| )
assume A1: g = f ; ::_thesis: for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th27;
now__::_thesis:_for_t_being_VECTOR_of_X_holds_||.(g_._t).||_<=_||.f.||_*_||.t.||
let t be VECTOR of X; ::_thesis: ||.(g . t).|| <= ||.f.|| * ||.t.||
now__::_thesis:_(_(_t_=_0._X_&_||.(g_._t).||_<=_||.f.||_*_||.t.||_)_or_(_t_<>_0._X_&_||.(g_._t).||_<=_||.f.||_*_||.t.||_)_)
percases ( t = 0. X or t <> 0. X ) ;
caseA3: t = 0. X ; ::_thesis: ||.(g . t).|| <= ||.f.|| * ||.t.||
then A4: ||.t.|| = 0 ;
g . t = g . (0 * (0. X)) by A3, RLVECT_1:10
.= 0 * (g . (0. X)) by Def5
.= 0. Y by RLVECT_1:10 ;
hence  ||.(g . t).|| <= ||.f.|| * ||.t.|| by A4; ::_thesis: verum
end;
caseA5: t <> 0. X ; ::_thesis: ||.(g . t).|| <= ||.f.|| * ||.t.||
reconsider t1 = (||.t.|| ") * t as VECTOR of X ;
A6: ||.t.|| <> 0 by A5, NORMSP_0:def_5;
A7: abs (||.t.|| ") = abs (1 * (||.t.|| "))
.= abs (1 / ||.t.||) by XCMPLX_0:def_9
.= 1 / (abs ||.t.||) by ABSVALUE:7
.= 1 / ||.t.|| by ABSVALUE:def_1
.= 1 * (||.t.|| ") by XCMPLX_0:def_9
.= ||.t.|| " ;
A8: ||.(g . t).|| / ||.t.|| = ||.(g . t).|| * (||.t.|| ") by XCMPLX_0:def_9
.= ||.((||.t.|| ") * (g . t)).|| by A7, NORMSP_1:def_1
.= ||.(g . t1).|| by Def5 ;
||.t1.|| = (abs (||.t.|| ")) * ||.t.|| by NORMSP_1:def_1
.= 1 by A6, A7, XCMPLX_0:def_7 ;
then  ||.(g . t).|| / ||.t.|| in  {  ||.(g . s).|| where s is VECTOR of X : ||.s.|| <= 1  }  by A8;
then  ||.(g . t).|| / ||.t.|| <= upper_bound (PreNorms g) by A2, SEQ_4:def_1;
then  ||.(g . t).|| / ||.t.|| <= (BoundedLinearOperatorsNorm (X,Y)) . g by Th30;
then A9: ||.(g . t).|| / ||.t.|| <= ||.f.|| by A1;
(||.(g . t).|| / ||.t.||) * ||.t.|| = (||.(g . t).|| * (||.t.|| ")) * ||.t.|| by XCMPLX_0:def_9
.= ||.(g . t).|| * ((||.t.|| ") * ||.t.||)
.= ||.(g . t).|| * 1 by A6, XCMPLX_0:def_7
.= ||.(g . t).|| ;
hence  ||.(g . t).|| <= ||.f.|| * ||.t.|| by A9, XREAL_1:64; ::_thesis: verum
end;
end;
end;
hence  ||.(g . t).|| <= ||.f.|| * ||.t.|| ; ::_thesis: verum
end;
hence  for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.|| ; ::_thesis: verum
end;

theorem Th33: :: LOPBAN_1:33
for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||
proof
let X, Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: 0 <= ||.f.||
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def9;
consider r0 being set  such that
A1: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A1;
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th27;
A3: (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms g) by Th30;
now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
0_<=_r
let r be Real; ::_thesis: ( r in PreNorms g implies 0 <= r )
assume  r in PreNorms g ; ::_thesis: 0 <= r
then  ex t being VECTOR of X st
( r = ||.(g . t).|| & ||.t.|| <= 1 ) ;
hence  0 <= r ; ::_thesis: verum
end;
then  0 <= r0 by A1;
then  0 <= upper_bound (PreNorms g) by A2, A1, SEQ_4:def_1;
hence  0 <= ||.f.|| by A3; ::_thesis: verum
end;

theorem Th34: :: LOPBAN_1:34
for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
0 = ||.f.||
proof
let X, Y be RealNormSpace; ::_thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
0 = ||.f.||
let f be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies 0 = ||.f.|| )
assume A1: f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ; ::_thesis: 0 = ||.f.||
thus  ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def9;
set z = the carrier of X --> (0. Y);
reconsider z = the carrier of X --> (0. Y) as Function of the carrier of X, the carrier of Y ;
consider r0 being set  such that
A2: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A2;
A3: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
A4: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th27;
A5: z = g by A1, Th31;
A6: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume  r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being VECTOR of X such that
A7: r = ||.(g . t).|| and
 ||.t.|| <= 1 ;
||.(g . t).|| = ||.(0. Y).|| by A5, FUNCOP_1:7
.= 0 ;
hence  ( 0 <= r & r <= 0 ) by A7; ::_thesis: verum
end;
then  0 <= r0 by A2;
then  upper_bound (PreNorms g) = 0 by A6, A4, A2, A3, SEQ_4:def_1;
then  (BoundedLinearOperatorsNorm (X,Y)) . f = 0 by Th30;
hence  ||.f.|| = 0 ; ::_thesis: verum
end;
end;

registration
let X, Y be RealNormSpace;
cluster  ->  Relation-like Function-like for Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y));
coherence
 for b1 being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( b1 is Function-like & b1 is Relation-like ) ;
end;

definition
let X, Y be RealNormSpace;
let f be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine funcf . v ->  VECTOR of Y;
coherence
 f . v is VECTOR of Y
proof
reconsider f = f as LinearOperator of X,Y by Def9;
 f . v is VECTOR of Y ;
hence  f . v is VECTOR of Y ; ::_thesis: verum
end;
end;

theorem Th35: :: LOPBAN_1:35
for X, Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof
let X, Y be RealNormSpace; ::_thesis: for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
let f, g, h be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
reconsider f1 = f, g1 = g, h1 = h as VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) ;
 ( h = f + g iff h1 = f1 + g1 ) ;
hence  ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) ) by Th24; ::_thesis: verum
end;

theorem Th36: :: LOPBAN_1:36
for X, Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof
let X, Y be RealNormSpace; ::_thesis: for f, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
let f, h be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
let a be Real; ::_thesis: ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
reconsider f1 = f as VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) ;
reconsider h1 = h as VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) ;
 ( h = a * f iff h1 = a * f1 ) ;
hence  ( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) ) by Th25; ::_thesis: verum
end;

theorem Th37: :: LOPBAN_1:37
for X, Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof
let X, Y be RealNormSpace; ::_thesis: for f, g being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let f, g be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let a be Real; ::_thesis: ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
A1: now__::_thesis:_(_f_=_0._(R_NormSpace_of_BoundedLinearOperators_(X,Y))_implies_||.f.||_=_0_)
assume A2: f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ; ::_thesis: ||.f.|| = 0
thus  ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def9;
set z = the carrier of X --> (0. Y);
reconsider z = the carrier of X --> (0. Y) as Function of the carrier of X, the carrier of Y ;
consider r0 being set  such that
A3: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A3;
A4: ( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;
A5: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th27;
A6: z = g by A2, Th31;
A7: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_g_holds_
(_0_<=_r_&_r_<=_0_)
let r be Real; ::_thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume  r in PreNorms g ; ::_thesis: ( 0 <= r & r <= 0 )
then consider t being VECTOR of X such that
A8: r = ||.(g . t).|| and
 ||.t.|| <= 1 ;
||.(g . t).|| = ||.(0. Y).|| by A6, FUNCOP_1:7
.= 0 ;
hence  ( 0 <= r & r <= 0 ) by A8; ::_thesis: verum
end;
then  0 <= r0 by A3;
then  upper_bound (PreNorms g) = 0 by A7, A5, A3, A4, SEQ_4:def_1;
then  (BoundedLinearOperatorsNorm (X,Y)) . f = 0 by Th30;
hence  ||.f.|| = 0 ; ::_thesis: verum
end;
end;
A9: ||.(f + g).|| <= ||.f.|| + ||.g.||
proof
reconsider f1 = f, g1 = g, h1 = f + g as Lipschitzian LinearOperator of X,Y by Def9;
A10: ( ( for s being real number st s in PreNorms h1 holds
s <= ||.f.|| + ||.g.|| ) implies upper_bound (PreNorms h1) <= ||.f.|| + ||.g.|| ) by SEQ_4:45;
A11: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.(h1_._t).||_<=_||.f.||_+_||.g.||
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.(h1 . t).|| <= ||.f.|| + ||.g.|| )
assume A12: ||.t.|| <= 1 ; ::_thesis: ||.(h1 . t).|| <= ||.f.|| + ||.g.||
 0 <= ||.g.|| by Th33;
then A13: ||.g.|| * ||.t.|| <= ||.g.|| * 1 by A12, XREAL_1:64;
 0 <= ||.f.|| by Th33;
then  ||.f.|| * ||.t.|| <= ||.f.|| * 1 by A12, XREAL_1:64;
then A14: (||.f.|| * ||.t.||) + (||.g.|| * ||.t.||) <= (||.f.|| * 1) + (||.g.|| * 1) by A13, XREAL_1:7;
A15: ||.((f1 . t) + (g1 . t)).|| <= ||.(f1 . t).|| + ||.(g1 . t).|| by NORMSP_1:def_1;
A16: ||.(g1 . t).|| <= ||.g.|| * ||.t.|| by Th32;
 ||.(f1 . t).|| <= ||.f.|| * ||.t.|| by Th32;
then  ||.(f1 . t).|| + ||.(g1 . t).|| <= (||.f.|| * ||.t.||) + (||.g.|| * ||.t.||) by A16, XREAL_1:7;
then A17: ||.(f1 . t).|| + ||.(g1 . t).|| <= ||.f.|| + ||.g.|| by A14, XXREAL_0:2;
 ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| by Th35;
hence  ||.(h1 . t).|| <= ||.f.|| + ||.g.|| by A15, A17, XXREAL_0:2; ::_thesis: verum
end;
A18: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_||.f.||_+_||.g.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= ||.f.|| + ||.g.|| )
assume  r in PreNorms h1 ; ::_thesis: r <= ||.f.|| + ||.g.||
then  ex t being VECTOR of X st
( r = ||.(h1 . t).|| & ||.t.|| <= 1 ) ;
hence  r <= ||.f.|| + ||.g.|| by A11; ::_thesis: verum
end;
 (BoundedLinearOperatorsNorm (X,Y)) . (f + g) = upper_bound (PreNorms h1) by Th30;
hence  ||.(f + g).|| <= ||.f.|| + ||.g.|| by A18, A10; ::_thesis: verum
end;
A19: ||.(a * f).|| = (abs a) * ||.f.||
proof
reconsider f1 = f, h1 = a * f as Lipschitzian LinearOperator of X,Y by Def9;
A20: ( ( for s being real number st s in PreNorms h1 holds
s <= (abs a) * ||.f.|| ) implies upper_bound (PreNorms h1) <= (abs a) * ||.f.|| ) by SEQ_4:45;
A21: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.(h1_._t).||_<=_(abs_a)_*_||.f.||
A22: 0 <= ||.f.|| by Th33;
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.(h1 . t).|| <= (abs a) * ||.f.|| )
assume  ||.t.|| <= 1 ; ::_thesis: ||.(h1 . t).|| <= (abs a) * ||.f.||
then A23: ||.f.|| * ||.t.|| <= ||.f.|| * 1 by A22, XREAL_1:64;
 ||.(f1 . t).|| <= ||.f.|| * ||.t.|| by Th32;
then A24: ||.(f1 . t).|| <= ||.f.|| by A23, XXREAL_0:2;
A25: ||.(a * (f1 . t)).|| = (abs a) * ||.(f1 . t).|| by NORMSP_1:def_1;
A26: 0 <= abs a by COMPLEX1:46;
 ||.(h1 . t).|| = ||.(a * (f1 . t)).|| by Th36;
hence  ||.(h1 . t).|| <= (abs a) * ||.f.|| by A25, A24, A26, XREAL_1:64; ::_thesis: verum
end;
A27: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_(abs_a)_*_||.f.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= (abs a) * ||.f.|| )
assume  r in PreNorms h1 ; ::_thesis: r <= (abs a) * ||.f.||
then  ex t being VECTOR of X st
( r = ||.(h1 . t).|| & ||.t.|| <= 1 ) ;
hence  r <= (abs a) * ||.f.|| by A21; ::_thesis: verum
end;
A28: now__::_thesis:_(_(_a_<>_0_&_(abs_a)_*_||.f.||_<=_||.(a_*_f).||_)_or_(_a_=_0_&_(abs_a)_*_||.f.||_=_||.(a_*_f).||_)_)
percases ( a <> 0 or a = 0 ) ;
caseA29: a <> 0 ; ::_thesis: (abs a) * ||.f.|| <= ||.(a * f).||
A30: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.(f1_._t).||_<=_((abs_a)_")_*_||.(a_*_f).||
A31: 0 <= ||.(a * f).|| by Th33;
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.(f1 . t).|| <= ((abs a) ") * ||.(a * f).|| )
assume  ||.t.|| <= 1 ; ::_thesis: ||.(f1 . t).|| <= ((abs a) ") * ||.(a * f).||
then A32: ||.(a * f).|| * ||.t.|| <= ||.(a * f).|| * 1 by A31, XREAL_1:64;
 ||.(h1 . t).|| <= ||.(a * f).|| * ||.t.|| by Th32;
then A33: ||.(h1 . t).|| <= ||.(a * f).|| by A32, XXREAL_0:2;
 h1 . t = a * (f1 . t) by Th36;
then A34: (a ") * (h1 . t) = ((a ") * a) * (f1 . t) by RLVECT_1:def_7
.= 1 * (f1 . t) by A29, XCMPLX_0:def_7
.= f1 . t by RLVECT_1:def_8 ;
A35: abs (a ") = abs (1 * (a "))
.= abs (1 / a) by XCMPLX_0:def_9
.= 1 / (abs a) by ABSVALUE:7
.= 1 * ((abs a) ") by XCMPLX_0:def_9
.= (abs a) " ;
A36: 0 <= abs (a ") by COMPLEX1:46;
 ||.((a ") * (h1 . t)).|| = (abs (a ")) * ||.(h1 . t).|| by NORMSP_1:def_1;
hence  ||.(f1 . t).|| <= ((abs a) ") * ||.(a * f).|| by A34, A33, A36, A35, XREAL_1:64; ::_thesis: verum
end;
A37: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_f1_holds_
r_<=_((abs_a)_")_*_||.(a_*_f).||
let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= ((abs a) ") * ||.(a * f).|| )
assume  r in PreNorms f1 ; ::_thesis: r <= ((abs a) ") * ||.(a * f).||
then  ex t being VECTOR of X st
( r = ||.(f1 . t).|| & ||.t.|| <= 1 ) ;
hence  r <= ((abs a) ") * ||.(a * f).|| by A30; ::_thesis: verum
end;
A38: ( ( for s being real number st s in PreNorms f1 holds
s <= ((abs a) ") * ||.(a * f).|| ) implies upper_bound (PreNorms f1) <= ((abs a) ") * ||.(a * f).|| ) by SEQ_4:45;
A39: 0 <= abs a by COMPLEX1:46;
 (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f1) by Th30;
then  ||.f.|| <= ((abs a) ") * ||.(a * f).|| by A37, A38;
then  (abs a) * ||.f.|| <= (abs a) * (((abs a) ") * ||.(a * f).||) by A39, XREAL_1:64;
then A40: (abs a) * ||.f.|| <= ((abs a) * ((abs a) ")) * ||.(a * f).|| ;
 abs a <> 0 by A29, COMPLEX1:47;
then  (abs a) * ||.f.|| <= 1 * ||.(a * f).|| by A40, XCMPLX_0:def_7;
hence  (abs a) * ||.f.|| <= ||.(a * f).|| ; ::_thesis: verum
end;
caseA41: a = 0 ; ::_thesis: (abs a) * ||.f.|| = ||.(a * f).||
reconsider fz = f as VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) ;
A42: a * f = a * fz
.= 0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) by A41, RLVECT_1:10
.= 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
thus (abs a) * ||.f.|| = 0 * ||.f.|| by A41, ABSVALUE:2
.= ||.(a * f).|| by A42, Th34 ; ::_thesis: verum
end;
end;
end;
 (BoundedLinearOperatorsNorm (X,Y)) . (a * f) = upper_bound (PreNorms h1) by Th30;
then  ||.(a * f).|| <= (abs a) * ||.f.|| by A27, A20;
hence  ||.(a * f).|| = (abs a) * ||.f.|| by A28, XXREAL_0:1; ::_thesis: verum
end;
now__::_thesis:_(_||.f.||_=_0_implies_f_=_0._(R_NormSpace_of_BoundedLinearOperators_(X,Y))_)
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def9;
set z = the carrier of X --> (0. Y);
reconsider z = the carrier of X --> (0. Y) as Function of the carrier of X, the carrier of Y ;
assume A43: ||.f.|| = 0 ; ::_thesis: f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y))
now__::_thesis:_for_t_being_VECTOR_of_X_holds_g_._t_=_z_._t
let t be VECTOR of X; ::_thesis: g . t = z . t
 ||.(g . t).|| <= ||.f.|| * ||.t.|| by Th32;
then  ||.(g . t).|| = 0 by A43;
hence g . t = 0. Y by NORMSP_0:def_5
.= z . t by FUNCOP_1:7 ;
::_thesis: verum
end;
then  g = z by FUNCT_2:63;
hence  f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) by Th31; ::_thesis: verum
end;
hence  ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A1, A19, A9; ::_thesis: verum
end;

theorem Th38: :: LOPBAN_1:38
for X, Y being RealNormSpace holds
( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like )
proof
let X, Y be RealNormSpace; ::_thesis: ( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like )
thus  ||.(0. (R_NormSpace_of_BoundedLinearOperators (X,Y))).|| = 0 by Th37; :: according to NORMSP_0:def_6 ::_thesis: ( R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like )
 for x, y being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( x = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th37;
hence  ( R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like ) by NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: verum
end;

theorem Th39: :: LOPBAN_1:39
for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace
proof
let X, Y be RealNormSpace; ::_thesis: R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace
 RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace ;
hence  R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace by Th38, RSSPACE3:2; ::_thesis: verum
end;

registration
let X, Y be RealNormSpace;
cluster R_NormSpace_of_BoundedLinearOperators (X,Y) ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
 ( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators (X,Y) is vector-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-unital & R_NormSpace_of_BoundedLinearOperators (X,Y) is Abelian & R_NormSpace_of_BoundedLinearOperators (X,Y) is add-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_zeroed & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_complementable ) by Th39;
end;

theorem Th40: :: LOPBAN_1:40
for X, Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
proof
let X, Y be RealNormSpace; ::_thesis: for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
let f, g, h be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
reconsider f9 = f, g9 = g, h9 = h as Lipschitzian LinearOperator of X,Y by Def9;
hereby  ::_thesis: ( ( for x being VECTOR of X holds h . x = (f . x) - (g . x) ) implies h = f - g )
assume  h = f - g ; ::_thesis: for x being VECTOR of X holds h . x = (f . x) - (g . x)
then  h + g = f - (g - g) by RLVECT_1:29;
then  h + g = f - (0. (R_NormSpace_of_BoundedLinearOperators (X,Y))) by RLVECT_1:15;
then A1: h + g = f by RLVECT_1:13;
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(f9_._x)_-_(g9_._x)_=_h9_._x
let x be VECTOR of X; ::_thesis: (f9 . x) - (g9 . x) = h9 . x
 f9 . x = (h9 . x) + (g9 . x) by A1, Th35;
then  (f9 . x) - (g9 . x) = (h9 . x) + ((g9 . x) - (g9 . x)) by RLVECT_1:def_3;
then  (f9 . x) - (g9 . x) = (h9 . x) + (0. Y) by RLVECT_1:15;
hence  (f9 . x) - (g9 . x) = h9 . x by RLVECT_1:4; ::_thesis: verum
end;
hence  for x being VECTOR of X holds h . x = (f . x) - (g . x) ; ::_thesis: verum
end;
assume A2: for x being VECTOR of X holds h . x = (f . x) - (g . x) ; ::_thesis: h = f - g
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(h9_._x)_+_(g9_._x)_=_f9_._x
let x be VECTOR of X; ::_thesis: (h9 . x) + (g9 . x) = f9 . x
 h9 . x = (f9 . x) - (g9 . x) by A2;
then  (h9 . x) + (g9 . x) = (f9 . x) - ((g9 . x) - (g9 . x)) by RLVECT_1:29;
then  (h9 . x) + (g9 . x) = (f9 . x) - (0. Y) by RLVECT_1:15;
hence  (h9 . x) + (g9 . x) = f9 . x by RLVECT_1:13; ::_thesis: verum
end;
then  f = h + g by Th35;
then  f - g = h + (g - g) by RLVECT_1:def_3;
then  f - g = h + (0. (R_NormSpace_of_BoundedLinearOperators (X,Y))) by RLVECT_1:15;
hence  h = f - g by RLVECT_1:4; ::_thesis: verum
end;

begin

definition
let X be RealNormSpace;
attrX is complete  means :Def15: :: LOPBAN_1:def 15
 for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent ;
end;

:: deftheorem Def15 defines complete LOPBAN_1:def_15_:_
 for X being RealNormSpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent );

registration
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() discerning reflexive RealNormSpace-like complete for NORMSTR ;
existence
 ex b1 being RealNormSpace st b1 is complete
proof
take  l1_Space ; ::_thesis: l1_Space is complete
thus  l1_Space is complete by Def15, RSSPACE3:9; ::_thesis: verum
end;
end;

definition
mode RealBanachSpace is complete RealNormSpace;
end;

Lm3:  for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
proof
let e be Real; ::_thesis: for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
let seq be Real_Sequence; ::_thesis: ( seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e implies lim seq <= e )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e ; ::_thesis: lim seq <= e
consider k being Element of NAT  such that
A3: for i being Element of NAT st k <= i holds
seq . i <= e by A2;
reconsider cseq = NAT --> e as Real_Sequence ;
A4: lim cseq = cseq . 0 by SEQ_4:26
.= e by FUNCOP_1:7 ;
A5: now__::_thesis:_for_i_being_Element_of_NAT_holds_(seq_^\_k)_._i_<=_cseq_._i
let i be Element of NAT ; ::_thesis: (seq ^\ k) . i <= cseq . i
A6: (seq ^\ k) . i = seq . (k + i) by NAT_1:def_3;
 seq . (k + i) <= e by A3, NAT_1:11;
hence  (seq ^\ k) . i <= cseq . i by A6, FUNCOP_1:7; ::_thesis: verum
end;
 lim (seq ^\ k) = lim seq by A1, SEQ_4:20;
hence  lim seq <= e by A1, A5, A4, SEQ_2:18; ::_thesis: verum
end;

theorem Th41: :: LOPBAN_1:41
for X being RealNormSpace
for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )
let seq be sequence of X; ::_thesis: ( seq is convergent implies ( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| ) )
assume A1: seq is convergent ; ::_thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )
A2: now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.seq.||_._m)_-_||.(lim_seq).||)_<_e1
let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.seq.|| . m) - ||.(lim seq).||) < e1 )
assume A3: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.seq.|| . m) - ||.(lim seq).||) < e1
reconsider e = e1 as Real by XREAL_0:def_1;
consider k being Element of NAT  such that
A4: for n being Element of NAT st n >= k holds
||.((seq . n) - (lim seq)).|| < e by A1, A3, NORMSP_1:def_7;
take k = k; ::_thesis: for m being Element of NAT st m >= k holds
abs ((||.seq.|| . m) - ||.(lim seq).||) < e1
now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.seq.||_._m)_-_||.(lim_seq).||)_<_e1
let m be Element of NAT ; ::_thesis: ( m >= k implies abs ((||.seq.|| . m) - ||.(lim seq).||) < e1 )
assume  m >= k ; ::_thesis: abs ((||.seq.|| . m) - ||.(lim seq).||) < e1
then A5: ||.((seq . m) - (lim seq)).|| < e by A4;
 ||.(seq . m).|| = ||.seq.|| . m by NORMSP_0:def_4;
then  abs ((||.seq.|| . m) - ||.(lim seq).||) <= ||.((seq . m) - (lim seq)).|| by NORMSP_1:9;
hence  abs ((||.seq.|| . m) - ||.(lim seq).||) < e1 by A5, XXREAL_0:2; ::_thesis: verum
end;
hence  for m being Element of NAT st m >= k holds
abs ((||.seq.|| . m) - ||.(lim seq).||) < e1 ; ::_thesis: verum
end;
then  ||.seq.|| is convergent by SEQ_2:def_6;
hence  ( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| ) by A2, SEQ_2:def_7; ::_thesis: verum
end;

theorem Th42: :: LOPBAN_1:42
for X, Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X, Y be RealNormSpace; ::_thesis: ( Y is complete implies for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent )
assume A1: Y is complete ; ::_thesis: for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means  ex xseq being sequence of Y st
( ( for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . $1 ) & xseq is convergent & $2 = lim xseq );
A3: for x being Element of X ex y being Element of Y st S1[x,y]
proof
let x be Element of X; ::_thesis: ex y being Element of Y st S1[x,y]
deffunc H1( Element of NAT ) ->  Element of the carrier of Y = (modetrans ((vseq . $1),X,Y)) . x;
consider xseq being sequence of Y such that
A4: for n being Element of NAT holds xseq . n = H1(n) from FUNCT_2:sch_4();
take  lim xseq ; ::_thesis: S1[x, lim xseq]
A5: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
proof
let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian LinearOperator of X,Y by Def9;
A6: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A4;
 vseq . m is Lipschitzian LinearOperator of X,Y by Def9;
then A7: modetrans ((vseq . m),X,Y) = vseq . m by Th29;
 vseq . k is Lipschitzian LinearOperator of X,Y by Def9;
then A8: modetrans ((vseq . k),X,Y) = vseq . k by Th29;
 xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4;
then  (xseq . m) - (xseq . k) = h1 . x by A7, A8, A6, Th40;
hence  ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th32; ::_thesis: verum
end;
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((xseq_._n)_-_(xseq_._m)).||_<_e
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e )
assume A9: e > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
now__::_thesis:_(_(_x_=_0._X_&_ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((xseq_._n)_-_(xseq_._m)).||_<_e_)_or_(_x_<>_0._X_&_ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((xseq_._n)_-_(xseq_._m)).||_<_e_)_)
percases ( x = 0. X or x <> 0. X ) ;
caseA10: x = 0. X ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
take k = 0 ; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
thus  for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum
proof
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume that
 n >= k and
 m >= k ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| < e
A11: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4
.= (modetrans ((vseq . m),X,Y)) . (0 * x) by A10, RLVECT_1:10
.= 0 * ((modetrans ((vseq . m),X,Y)) . x) by Def5
.= 0. Y by RLVECT_1:10 ;
xseq . n = (modetrans ((vseq . n),X,Y)) . x by A4
.= (modetrans ((vseq . n),X,Y)) . (0 * x) by A10, RLVECT_1:10
.= 0 * ((modetrans ((vseq . n),X,Y)) . x) by Def5
.= 0. Y by RLVECT_1:10 ;
then ||.((xseq . n) - (xseq . m)).|| = ||.(0. Y).|| by A11, RLVECT_1:13
.= 0 ;
hence  ||.((xseq . n) - (xseq . m)).|| < e by A9; ::_thesis: verum
end;
end;
case x <> 0. X ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
then A12: ||.x.|| <> 0 by NORMSP_0:def_5;
then A13: ||.x.|| > 0 ;
then  e / ||.x.|| > 0 by A9, XREAL_1:139;
then consider k being Element of NAT  such that
A14: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e / ||.x.|| by A2, RSSPACE3:8;
take k = k; ::_thesis: for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e
thus  for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ::_thesis: verum
proof
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((xseq . n) - (xseq . m)).|| < e )
assume that
A15: n >= k and
A16: m >= k ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| < e
 ||.((vseq . n) - (vseq . m)).|| < e / ||.x.|| by A14, A15, A16;
then A17: ||.((vseq . n) - (vseq . m)).|| * ||.x.|| < (e / ||.x.||) * ||.x.|| by A13, XREAL_1:68;
A18: (e / ||.x.||) * ||.x.|| = (e * (||.x.|| ")) * ||.x.|| by XCMPLX_0:def_9
.= e * ((||.x.|| ") * ||.x.||)
.= e * 1 by A12, XCMPLX_0:def_7
.= e ;
 ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * ||.x.|| by A5;
hence  ||.((xseq . n) - (xseq . m)).|| < e by A17, A18, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
hence  ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((xseq . n) - (xseq . m)).|| < e ; ::_thesis: verum
end;
then  xseq is Cauchy_sequence_by_Norm by RSSPACE3:8;
then  xseq is convergent by A1, Def15;
hence  S1[x, lim xseq] by A4; ::_thesis: verum
end;
consider f being Function of the carrier of X, the carrier of Y such that
A19: for x being Element of X holds S1[x,f . x] from FUNCT_2:sch_3(A3);
reconsider tseq = f as Function of X,Y ;
A20: now__::_thesis:_for_x,_y_being_VECTOR_of_X_holds_tseq_._(x_+_y)_=_(tseq_._x)_+_(tseq_._y)
let x, y be VECTOR of X; ::_thesis: tseq . (x + y) = (tseq . x) + (tseq . y)
consider xseq being sequence of Y such that
A21: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A22: xseq is convergent and
A23: tseq . x = lim xseq by A19;
consider zseq being sequence of Y such that
A24: for n being Element of NAT holds zseq . n = (modetrans ((vseq . n),X,Y)) . (x + y) and
 zseq is convergent and
A25: tseq . (x + y) = lim zseq by A19;
consider yseq being sequence of Y such that
A26: for n being Element of NAT holds yseq . n = (modetrans ((vseq . n),X,Y)) . y and
A27: yseq is convergent and
A28: tseq . y = lim yseq by A19;
now__::_thesis:_for_n_being_Element_of_NAT_holds_zseq_._n_=_(xseq_._n)_+_(yseq_._n)
let n be Element of NAT ; ::_thesis: zseq . n = (xseq . n) + (yseq . n)
thus zseq . n = (modetrans ((vseq . n),X,Y)) . (x + y) by A24
.= ((modetrans ((vseq . n),X,Y)) . x) + ((modetrans ((vseq . n),X,Y)) . y) by VECTSP_1:def_20
.= (xseq . n) + ((modetrans ((vseq . n),X,Y)) . y) by A21
.= (xseq . n) + (yseq . n) by A26 ; ::_thesis: verum
end;
then  zseq = xseq + yseq by NORMSP_1:def_2;
hence  tseq . (x + y) = (tseq . x) + (tseq . y) by A22, A23, A27, A28, A25, NORMSP_1:25; ::_thesis: verum
end;
now__::_thesis:_for_x_being_VECTOR_of_X
for_a_being_Real_holds_tseq_._(a_*_x)_=_a_*_(tseq_._x)
let x be VECTOR of X; ::_thesis: for a being Real holds tseq . (a * x) = a * (tseq . x)
let a be Real; ::_thesis: tseq . (a * x) = a * (tseq . x)
consider xseq being sequence of Y such that
A29: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A30: xseq is convergent and
A31: tseq . x = lim xseq by A19;
consider zseq being sequence of Y such that
A32: for n being Element of NAT holds zseq . n = (modetrans ((vseq . n),X,Y)) . (a * x) and
 zseq is convergent and
A33: tseq . (a * x) = lim zseq by A19;
now__::_thesis:_for_n_being_Element_of_NAT_holds_zseq_._n_=_a_*_(xseq_._n)
let n be Element of NAT ; ::_thesis: zseq . n = a * (xseq . n)
thus zseq . n = (modetrans ((vseq . n),X,Y)) . (a * x) by A32
.= a * ((modetrans ((vseq . n),X,Y)) . x) by Def5
.= a * (xseq . n) by A29 ; ::_thesis: verum
end;
then  zseq = a * xseq by NORMSP_1:def_5;
hence  tseq . (a * x) = a * (tseq . x) by A30, A31, A33, NORMSP_1:28; ::_thesis: verum
end;
then reconsider tseq = tseq as LinearOperator of X,Y by A20, Def5, VECTSP_1:def_20;
now__::_thesis:_for_e1_being_real_number_st_e1_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let e1 be real number ; ::_thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume A34: e1 > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
reconsider e = e1 as Real by XREAL_0:def_1;
consider k being Element of NAT  such that
A35: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, A34, RSSPACE3:8;
take k = k; ::_thesis: for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
now__::_thesis:_for_m_being_Element_of_NAT_st_m_>=_k_holds_
abs_((||.vseq.||_._m)_-_(||.vseq.||_._k))_<_e1
let m be Element of NAT ; ::_thesis: ( m >= k implies abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 )
assume  m >= k ; ::_thesis: abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1
then A36: ||.((vseq . m) - (vseq . k)).|| < e by A35;
A37: ||.(vseq . m).|| = ||.vseq.|| . m by NORMSP_0:def_4;
A38: ||.(vseq . k).|| = ||.vseq.|| . k by NORMSP_0:def_4;
 abs (||.(vseq . m).|| - ||.(vseq . k).||) <= ||.((vseq . m) - (vseq . k)).|| by NORMSP_1:9;
hence  abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 by A38, A37, A36, XXREAL_0:2; ::_thesis: verum
end;
hence  for m being Element of NAT st m >= k holds
abs ((||.vseq.|| . m) - (||.vseq.|| . k)) < e1 ; ::_thesis: verum
end;
then A39: ||.vseq.|| is convergent by SEQ_4:41;
A40: tseq is Lipschitzian
proof
take  lim ||.vseq.|| ; :: according to LOPBAN_1:def_8 ::_thesis: ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X holds ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| ) )
A41: now__::_thesis:_for_x_being_VECTOR_of_X_holds_||.(tseq_._x).||_<=_(lim_||.vseq.||)_*_||.x.||
let x be VECTOR of X; ::_thesis: ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.||
consider xseq being sequence of Y such that
A42: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A43: xseq is convergent and
A44: tseq . x = lim xseq by A19;
A45: ||.(tseq . x).|| = lim ||.xseq.|| by A43, A44, Th20;
A46: for m being Element of NAT holds ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||
proof
let m be Element of NAT ; ::_thesis: ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.||
A47: xseq . m = (modetrans ((vseq . m),X,Y)) . x by A42;
 vseq . m is Lipschitzian LinearOperator of X,Y by Def9;
hence  ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.|| by A47, Th29, Th32; ::_thesis: verum
end;
A48: for n being Element of NAT holds ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n
proof
let n be Element of NAT ; ::_thesis: ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n
A49: ||.xseq.|| . n = ||.(xseq . n).|| by NORMSP_0:def_4;
A50: ||.(vseq . n).|| = ||.vseq.|| . n by NORMSP_0:def_4;
 ||.(xseq . n).|| <= ||.(vseq . n).|| * ||.x.|| by A46;
hence  ||.xseq.|| . n <= (||.x.|| (#) ||.vseq.||) . n by A49, A50, SEQ_1:9; ::_thesis: verum
end;
A51: ||.x.|| (#) ||.vseq.|| is convergent by A39, SEQ_2:7;
A52: lim (||.x.|| (#) ||.vseq.||) = (lim ||.vseq.||) * ||.x.|| by A39, SEQ_2:8;
 ||.xseq.|| is convergent by A43, A44, Th20;
hence  ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| by A45, A48, A51, A52, SEQ_2:18; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.vseq.||_._n_>=_0
let n be Element of NAT ; ::_thesis: ||.vseq.|| . n >= 0
 ||.(vseq . n).|| >= 0 ;
hence  ||.vseq.|| . n >= 0 by NORMSP_0:def_4; ::_thesis: verum
end;
hence  ( 0 <= lim ||.vseq.|| & ( for x being VECTOR of X holds ||.(tseq . x).|| <= (lim ||.vseq.||) * ||.x.|| ) ) by A39, A41, SEQ_2:17; ::_thesis: verum
end;
A53: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| )
assume  e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
then consider k being Element of NAT  such that
A54: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, RSSPACE3:8;
take  k ; ::_thesis: for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
for_x_being_VECTOR_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e_*_||.x.||
let n be Element of NAT ; ::_thesis: ( n >= k implies for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| )
assume A55: n >= k ; ::_thesis: for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
now__::_thesis:_for_x_being_VECTOR_of_X_holds_||.(((modetrans_((vseq_._n),X,Y))_._x)_-_(tseq_._x)).||_<=_e_*_||.x.||
let x be VECTOR of X; ::_thesis: ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.||
consider xseq being sequence of Y such that
A56: for n being Element of NAT holds xseq . n = (modetrans ((vseq . n),X,Y)) . x and
A57: xseq is convergent and
A58: tseq . x = lim xseq by A19;
A59: for m, k being Element of NAT holds ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
proof
let m, k be Element of NAT ; ::_thesis: ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.||
reconsider h1 = (vseq . m) - (vseq . k) as Lipschitzian LinearOperator of X,Y by Def9;
A60: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A56;
 vseq . m is Lipschitzian LinearOperator of X,Y by Def9;
then A61: modetrans ((vseq . m),X,Y) = vseq . m by Th29;
 vseq . k is Lipschitzian LinearOperator of X,Y by Def9;
then A62: modetrans ((vseq . k),X,Y) = vseq . k by Th29;
 xseq . m = (modetrans ((vseq . m),X,Y)) . x by A56;
then  (xseq . m) - (xseq . k) = h1 . x by A61, A62, A60, Th40;
hence  ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th32; ::_thesis: verum
end;
A63: for m being Element of NAT st m >= k holds
||.((xseq . n) - (xseq . m)).|| <= e * ||.x.||
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies ||.((xseq . n) - (xseq . m)).|| <= e * ||.x.|| )
assume  m >= k ; ::_thesis: ||.((xseq . n) - (xseq . m)).|| <= e * ||.x.||
then A64: ||.((vseq . n) - (vseq . m)).|| < e by A54, A55;
A65: ||.((xseq . n) - (xseq . m)).|| <= ||.((vseq . n) - (vseq . m)).|| * ||.x.|| by A59;
 ||.((vseq . n) - (vseq . m)).|| * ||.x.|| <= e * ||.x.|| by A64, XREAL_1:64;
hence  ||.((xseq . n) - (xseq . m)).|| <= e * ||.x.|| by A65, XXREAL_0:2; ::_thesis: verum
end;
 ||.((xseq . n) - (tseq . x)).|| <= e * ||.x.||
proof
deffunc H1( Element of NAT ) ->  Element of REAL = ||.((xseq . $1) - (xseq . n)).||;
consider rseq being Real_Sequence such that
A66: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
rseq_._x_=_||.(xseq_-_(xseq_._n)).||_._x
let x be set ; ::_thesis: ( x in NAT implies rseq . x = ||.(xseq - (xseq . n)).|| . x )
assume  x in NAT ; ::_thesis: rseq . x = ||.(xseq - (xseq . n)).|| . x
then reconsider k = x as Element of NAT ;
thus rseq . x = ||.((xseq . k) - (xseq . n)).|| by A66
.= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def_4
.= ||.(xseq - (xseq . n)).|| . x by NORMSP_0:def_4 ; ::_thesis: verum
end;
then A67: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2:12;
A68: xseq - (xseq . n) is convergent by A57, NORMSP_1:21;
 lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by A57, A58, NORMSP_1:27;
then A69: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A68, A67, Th41;
 for m being Element of NAT st m >= k holds
rseq . m <= e * ||.x.||
proof
let m be Element of NAT ; ::_thesis: ( m >= k implies rseq . m <= e * ||.x.|| )
assume A70: m >= k ; ::_thesis: rseq . m <= e * ||.x.||
rseq . m = ||.((xseq . m) - (xseq . n)).|| by A66
.= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1:7 ;
hence  rseq . m <= e * ||.x.|| by A63, A70; ::_thesis: verum
end;
then  lim rseq <= e * ||.x.|| by A68, A67, Lm3, Th41;
hence  ||.((xseq . n) - (tseq . x)).|| <= e * ||.x.|| by A69, NORMSP_1:7; ::_thesis: verum
end;
hence  ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| by A56; ::_thesis: verum
end;
hence  for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| ; ::_thesis: verum
end;
hence  for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| ; ::_thesis: verum
end;
reconsider tseq = tseq as Lipschitzian LinearOperator of X,Y by A40;
reconsider tv = tseq as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by Def9;
A71: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
proof
let e be Real; ::_thesis: ( e > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e )
assume A72: e > 0 ; ::_thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e
consider k being Element of NAT  such that
A73: for n being Element of NAT st n >= k holds
for x being VECTOR of X holds ||.(((modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= e * ||.x.|| by A53, A72;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_k_holds_
||.((vseq_._n)_-_tv).||_<=_e
set g1 = tseq;
let n be Element of NAT ; ::_thesis: ( n >= k implies ||.((vseq . n) - tv).|| <= e )
assume A74: n >= k ; ::_thesis: ||.((vseq . n) - tv).|| <= e
reconsider h1 = (vseq . n) - tv as Lipschitzian LinearOperator of X,Y by Def9;
set f1 = modetrans ((vseq . n),X,Y);
A75: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.(h1_._t).||_<=_e
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.(h1 . t).|| <= e )
assume  ||.t.|| <= 1 ; ::_thesis: ||.(h1 . t).|| <= e
then A76: e * ||.t.|| <= e * 1 by A72, XREAL_1:64;
A77: ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| <= e * ||.t.|| by A73, A74;
 vseq . n is Lipschitzian LinearOperator of X,Y by Def9;
then  modetrans ((vseq . n),X,Y) = vseq . n by Th29;
then  ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th40;
hence  ||.(h1 . t).|| <= e by A77, A76, XXREAL_0:2; ::_thesis: verum
end;
A78: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_h1_holds_
r_<=_e
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= e )
assume  r in PreNorms h1 ; ::_thesis: r <= e
then  ex t being VECTOR of X st
( r = ||.(h1 . t).|| & ||.t.|| <= 1 ) ;
hence  r <= e by A75; ::_thesis: verum
end;
A79: ( ( for s being real number st s in PreNorms h1 holds
s <= e ) implies upper_bound (PreNorms h1) <= e ) by SEQ_4:45;
 (BoundedLinearOperatorsNorm (X,Y)) . ((vseq . n) - tv) = upper_bound (PreNorms h1) by Th30;
hence  ||.((vseq . n) - tv).|| <= e by A78, A79; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n being Element of NAT st n >= k holds
||.((vseq . n) - tv).|| <= e ; ::_thesis: verum
end;
 for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
proof
let e be Real; ::_thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A80: e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT  such that
A81: for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| <= e / 2 by A71, A80, XREAL_1:215;
A82: e / 2 < e by A80, XREAL_1:216;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume  n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
then  ||.((vseq . n) - tv).|| <= e / 2 by A81;
hence  ||.((vseq . n) - tv).|| < e by A82, XXREAL_0:2; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; ::_thesis: verum
end;
hence  vseq is convergent by NORMSP_1:def_6; ::_thesis: verum
end;

theorem Th43: :: LOPBAN_1:43
for X being RealNormSpace
for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace
proof
let X be RealNormSpace; ::_thesis: for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace
let Y be RealBanachSpace; ::_thesis: R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace
 for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th42;
hence  R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace by Def15; ::_thesis: verum
end;

registration
let X be RealNormSpace;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedLinearOperators (X,Y) ->  non empty complete ;
coherence
 R_NormSpace_of_BoundedLinearOperators (X,Y) is complete by Th43;
end;