:: CLOPBAN1 semantic presentation

begin

definition
let X be set ;
let Y be non empty set ;
let F be Function of [:COMPLEX,Y:],Y;
let c be complex number ;
let f be Function of X,Y;
:: original: [;]
redefine funcF [;] (c,f) ->  Element of Funcs (X,Y);
coherence
 F [;] (c,f) is Element of Funcs (X,Y)
proof
A1: dom f = X by FUNCT_2:def_1;
 c in COMPLEX by XCMPLX_0:def_2;
then  (dom f) --> c is Function of X,COMPLEX by A1, FUNCOP_1:45;
then reconsider g = <:((dom f) --> c),f:> as Function of X,[:COMPLEX,Y:] by FUNCT_3:58;
 F [;] (c,f) = F * g by FUNCOP_1:def_5;
hence  F [;] (c,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 ComplexLinearSpace;
func FuncExtMult (X,Y) ->  Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) means :Def1: :: CLOPBAN1:def 1
 for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it . [c,f]) . x = c * (f . x);
existence
 ex b1 being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [c,f]) . x = c * (f . x)
proof
deffunc H1( Complex, 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 [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) such that
A1: for c being Element of COMPLEX
for f being Element of Funcs (X, the carrier of Y) holds F . (c,f) = H1(c,f) from BINOP_1:sch_4();
take  F ; ::_thesis: for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (F . [c,f]) . x = c * (f . x)
let c be Complex; ::_thesis: for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (F . [c,f]) . x = c * (f . x)
let f be Element of Funcs (X, the carrier of Y); ::_thesis: for x being Element of X holds (F . [c,f]) . x = c * (f . x)
let x be Element of X; ::_thesis: (F . [c,f]) . x = c * (f . x)
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def_2;
A2: dom (F . [c1,f]) = X by FUNCT_2:92;
 F . (c1,f) = the Mult of Y [;] (c1,f) by A1;
hence (F . [c,f]) . x = the Mult of Y . (c,(f . x)) by A2, FUNCOP_1:32
.= c * (f . x) by CLVECT_1:def_1 ;
::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st ( for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [c,f]) . x = c * (f . x) ) & ( for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b2 . [c,f]) . x = c * (f . x) ) holds
b1 = b2
proof
let it1, it2 be Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)); ::_thesis: ( ( for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it1 . [c,f]) . x = c * (f . x) ) & ( for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it2 . [c,f]) . x = c * (f . x) ) implies it1 = it2 )
assume that
A3: for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it1 . [c,f]) . x = c * (f . x) and
A4: for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it2 . [c,f]) . x = c * (f . x) ; ::_thesis: it1 = it2
now__::_thesis:_for_c_being_Element_of_COMPLEX_
for_f_being_Element_of_Funcs_(X,_the_carrier_of_Y)_holds_it1_._(c,f)_=_it2_._(c,f)
let c be Element of COMPLEX ; ::_thesis: for f being Element of Funcs (X, the carrier of Y) holds it1 . (c,f) = it2 . (c,f)
let f be Element of Funcs (X, the carrier of Y); ::_thesis: it1 . (c,f) = it2 . (c,f)
now__::_thesis:_for_x_being_Element_of_X_holds_(it1_._[c,f])_._x_=_(it2_._[c,f])_._x
let x be Element of X; ::_thesis: (it1 . [c,f]) . x = (it2 . [c,f]) . x
thus (it1 . [c,f]) . x = c * (f . x) by A3
.= (it2 . [c,f]) . x by A4 ; ::_thesis: verum
end;
hence  it1 . (c,f) = it2 . (c,f) by FUNCT_2:63; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines FuncExtMult CLOPBAN1:def_1_:_
 for X being non empty set
for Y being ComplexLinearSpace
for b3 being Function of [:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) holds
( b3 = FuncExtMult (X,Y) iff for c being Complex
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b3 . [c,f]) . x = c * (f . x) );


theorem Th1: :: CLOPBAN1:1
for X being non empty set
for Y being ComplexLinearSpace
for x being Element of X holds (FuncZero (X,Y)) . x = 0. Y
proof
let X be non empty set ; ::_thesis: for Y being ComplexLinearSpace
for x being Element of X holds (FuncZero (X,Y)) . x = 0. Y
let Y be ComplexLinearSpace; ::_thesis: for x being Element of X holds (FuncZero (X,Y)) . x = 0. Y
let x be Element of X; ::_thesis: (FuncZero (X,Y)) . x = 0. Y
thus (FuncZero (X,Y)) . x = (X --> (0. Y)) . x by LOPBAN_1:def_3
.= 0. Y by FUNCOP_1:7 ; ::_thesis: verum
end;


theorem Th2: :: CLOPBAN1:2
for X being non empty set
for Y being ComplexLinearSpace
for h, f being Element of Funcs (X, the carrier of Y)
for a being Complex 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 ComplexLinearSpace
for h, f being Element of Funcs (X, the carrier of Y)
for a being Complex holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let Y be ComplexLinearSpace; ::_thesis: for h, f being Element of Funcs (X, the carrier of Y)
for a being Complex 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 Complex holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
let a be Complex; ::_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 Def1; ::_thesis: ( ( for x being Element of X holds h . x = a * (f . x) ) implies h = (FuncExtMult (X,Y)) . [a,f] )
reconsider a = a as Element of COMPLEX by XCMPLX_0:def_2;
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 Def1 ; ::_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: :: CLOPBAN1:3
for X being non empty set
for Y being ComplexLinearSpace
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 ComplexLinearSpace
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 ComplexLinearSpace; ::_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 LOPBAN_1:1
.= ((FuncAdd (X,Y)) . (g,f)) . x by LOPBAN_1:1 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th4: :: CLOPBAN1:4
for X being non empty set
for Y being ComplexLinearSpace
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 ComplexLinearSpace
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 ComplexLinearSpace; ::_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 LOPBAN_1:1
.= (f . x) + ((g . x) + (h . x)) by LOPBAN_1:1
.= ((f . x) + (g . x)) + (h . x) by RLVECT_1:def_3
.= (((FuncAdd (X,Y)) . (f,g)) . x) + (h . x) by LOPBAN_1:1
.= ((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)) . x by LOPBAN_1:1 ; ::_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: :: CLOPBAN1:5
for X being non empty set
for Y being ComplexLinearSpace
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 ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f
let Y be ComplexLinearSpace; ::_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 LOPBAN_1:1
.= (0. Y) + (f . x) by Th1
.= 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: :: CLOPBAN1:6
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)
proof
let X be non empty set ; ::_thesis: for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)
let Y be ComplexLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)
let f be Element of Funcs (X, the carrier of Y); ::_thesis: (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y)
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(f,((FuncExtMult_(X,Y))_._[(-_1r),f])))_._x_=_(FuncZero_(X,Y))_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f]))) . x = (FuncZero (X,Y)) . x
set y = f . x;
thus ((FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f]))) . x = (f . x) + (((FuncExtMult (X,Y)) . [(- 1r),f]) . x) by LOPBAN_1:1
.= (f . x) + ((- 1r) * (f . x)) by Th2
.= (f . x) + (- (f . x)) by CLVECT_1:3
.= 0. Y by RLVECT_1:5
.= (FuncZero (X,Y)) . x by Th1 ; ::_thesis: verum
end;
hence  (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1r),f])) = FuncZero (X,Y) by FUNCT_2:63; ::_thesis: verum
end;

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

theorem Th8: :: CLOPBAN1:8
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex 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 ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
let Y be ComplexLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex 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 Complex holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
let a, b be Complex; ::_thesis: (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def_2;
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncExtMult_(X,Y))_._[a1,((FuncExtMult_(X,Y))_._[b1,f])])_._x_=_((FuncExtMult_(X,Y))_._[(a1_*_b1),f])_._x
let x be Element of X; ::_thesis: ((FuncExtMult (X,Y)) . [a1,((FuncExtMult (X,Y)) . [b1,f])]) . x = ((FuncExtMult (X,Y)) . [(a1 * b1),f]) . x
thus ((FuncExtMult (X,Y)) . [a1,((FuncExtMult (X,Y)) . [b1,f])]) . x = a1 * (((FuncExtMult (X,Y)) . [b1,f]) . x) by Th2
.= a * (b * (f . x)) by Th2
.= (a * b) * (f . x) by CLVECT_1:def_4
.= ((FuncExtMult (X,Y)) . [(a1 * b1),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: :: CLOPBAN1:9
for X being non empty set
for Y being ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex 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 ComplexLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let Y be ComplexLinearSpace; ::_thesis: for f being Element of Funcs (X, the carrier of Y)
for a, b being Complex 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 Complex holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
let a, b be Complex; ::_thesis: (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def_2;
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(((FuncExtMult_(X,Y))_._[a1,f]),((FuncExtMult_(X,Y))_._[b1,f])))_._x_=_((FuncExtMult_(X,Y))_._[(a1_+_b1),f])_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a1,f]),((FuncExtMult (X,Y)) . [b1,f]))) . x = ((FuncExtMult (X,Y)) . [(a1 + b1),f]) . x
thus ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a1,f]),((FuncExtMult (X,Y)) . [b1,f]))) . x = (((FuncExtMult (X,Y)) . [a1,f]) . x) + (((FuncExtMult (X,Y)) . [b1,f]) . x) by LOPBAN_1:1
.= (a1 * (f . x)) + (((FuncExtMult (X,Y)) . [b1,f]) . x) by Th2
.= (a * (f . x)) + (b * (f . x)) by Th2
.= (a + b) * (f . x) by CLVECT_1:def_3
.= ((FuncExtMult (X,Y)) . [(a1 + b1),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;

Lm1:  for X being non empty set
for Y being ComplexLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Complex 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 ComplexLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Complex 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 ComplexLinearSpace; ::_thesis: for f, g being Element of Funcs (X, the carrier of Y)
for a being Complex 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 Complex 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 Complex; ::_thesis: (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def_2;
now__::_thesis:_for_x_being_Element_of_X_holds_((FuncAdd_(X,Y))_._(((FuncExtMult_(X,Y))_._[a1,f]),((FuncExtMult_(X,Y))_._[a1,g])))_._x_=_((FuncExtMult_(X,Y))_._[a1,((FuncAdd_(X,Y))_._(f,g))])_._x
let x be Element of X; ::_thesis: ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a1,f]),((FuncExtMult (X,Y)) . [a1,g]))) . x = ((FuncExtMult (X,Y)) . [a1,((FuncAdd (X,Y)) . (f,g))]) . x
thus ((FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a1,f]),((FuncExtMult (X,Y)) . [a1,g]))) . x = (((FuncExtMult (X,Y)) . [a1,f]) . x) + (((FuncExtMult (X,Y)) . [a1,g]) . x) by LOPBAN_1:1
.= (a1 * (f . x)) + (((FuncExtMult (X,Y)) . [a1,g]) . x) by Th2
.= (a * (f . x)) + (a * (g . x)) by Th2
.= a * ((f . x) + (g . x)) by CLVECT_1:def_2
.= a * (((FuncAdd (X,Y)) . (f,g)) . x) by LOPBAN_1:1
.= ((FuncExtMult (X,Y)) . [a1,((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: :: CLOPBAN1:10
for X being non empty set
for Y being ComplexLinearSpace holds CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace
proof
let X be non empty set ; ::_thesis: for Y being ComplexLinearSpace holds CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace
let Y be ComplexLinearSpace; ::_thesis: CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace
set IT = CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);
A1: for u, v, w being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (u + v) + w = u + (v + w) by Th4;
A2: for u being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds u is right_complementable
proof
let u be VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); ::_thesis: u is right_complementable
reconsider u9 = u as Element of Funcs (X, the carrier of Y) ;
reconsider w = (FuncExtMult (X,Y)) . [(- 1r),u9] as VECTOR of CLSStruct(# (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. CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)
thus  u + w = 0. CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) by Th6; ::_thesis: verum
end;
A3: for a being Complex
for u, v being VECTOR of CLSStruct(# (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 Complex; ::_thesis: for u, v being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds a * (u + v) = (a * u) + (a * v)
let u, v be VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); ::_thesis: a * (u + v) = (a * u) + (a * v)
reconsider a = a as Element of COMPLEX by XCMPLX_0:def_2;
 a * (u + v) = (a * u) + (a * v)
proof
reconsider v9 = v, u9 = u as Element of Funcs (X, the carrier of Y) ;
reconsider w = (FuncExtMult (X,Y)) . [a,u9], w9 = (FuncExtMult (X,Y)) . [a,v9] as VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) ;
a * (u + v) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (u9,v9))] by CLVECT_1:def_1
.= (FuncAdd (X,Y)) . (w,w9) by Lm1
.= w + (a * v) by CLVECT_1:def_1
.= (a * u) + (a * v) by CLVECT_1:def_1 ;
hence  a * (u + v) = (a * u) + (a * v) ; ::_thesis: verum
end;
hence  a * (u + v) = (a * u) + (a * v) ; ::_thesis: verum
end;
A4: for a, b being Complex
for v being VECTOR of CLSStruct(# (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 Complex; ::_thesis: for v being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a * b) * v = a * (b * v)
let v be VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); ::_thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as Element of Funcs (X, the carrier of Y) ;
thus (a * b) * v = (FuncExtMult (X,Y)) . [(a * b),v9] by CLVECT_1:def_1
.= (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,v9])] by Th8
.= (FuncExtMult (X,Y)) . [a,(b * v)] by CLVECT_1:def_1
.= a * (b * v) by CLVECT_1:def_1 ; ::_thesis: verum
end;
A5: for a, b being Complex
for v being VECTOR of CLSStruct(# (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 Complex; ::_thesis: for v being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def_2;
reconsider v9 = v as Element of Funcs (X, the carrier of Y) ;
reconsider w = (FuncExtMult (X,Y)) . [a,v9], w9 = (FuncExtMult (X,Y)) . [b,v9] as VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) ;
(a + b) * v = (FuncExtMult (X,Y)) . [(a + b),v9] by CLVECT_1:def_1
.= (FuncAdd (X,Y)) . (w,w9) by Th9
.= w + (b * v) by CLVECT_1:def_1
.= (a * v) + (b * v) by CLVECT_1:def_1 ;
hence  (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
A6: for u being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds u + (0. CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #)) = u
proof
let u be VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); ::_thesis: u + (0. CLSStruct(# (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. CLSStruct(# (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;
A7: for v being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds 1r * v = v
proof
let v be VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #); ::_thesis: 1r * v = v
reconsider v9 = v as Element of Funcs (X, the carrier of Y) ;
thus 1r * v = (FuncExtMult (X,Y)) . [1r,v9] by CLVECT_1:def_1
.= v by Th7 ; ::_thesis: verum
end;
 for u, v being VECTOR of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) holds u + v = v + u by Th3;
hence  CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace by A1, A6, A2, A3, A5, A4, A7, ALGSTR_0:def_16, CLVECT_1:def_2, CLVECT_1:def_3, CLVECT_1:def_4, CLVECT_1:def_5, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4; ::_thesis: verum
end;

definition
let X be non empty set ;
let Y be ComplexLinearSpace;
func ComplexVectSpace (X,Y) ->  ComplexLinearSpace equals :: CLOPBAN1:def 2
 CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);
coherence
 CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is ComplexLinearSpace by Th10;
end;

:: deftheorem  defines ComplexVectSpace CLOPBAN1:def_2_:_
 for X being non empty set
for Y being ComplexLinearSpace holds ComplexVectSpace (X,Y) = CLSStruct(# (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 ComplexLinearSpace;
cluster ComplexVectSpace (X,Y) ->  strict ;
coherence
 ComplexVectSpace (X,Y) is strict ;
end;

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

definition
let X be non empty set ;
let Y be ComplexLinearSpace;
let f be VECTOR of (ComplexVectSpace (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 :: CLOPBAN1:11
for X being non empty set
for Y being ComplexLinearSpace
for f, g, h being VECTOR of (ComplexVectSpace (X,Y)) holds
( h = f + g iff for x being Element of X holds h . x = (f . x) + (g . x) ) by LOPBAN_1:1;

theorem Th12: :: CLOPBAN1:12
for X being non empty set
for Y being ComplexLinearSpace
for f, h being VECTOR of (ComplexVectSpace (X,Y))
for c being Complex holds
( h = c * f iff for x being Element of X holds h . x = c * (f . x) )
proof
let X be non empty set ; ::_thesis: for Y being ComplexLinearSpace
for f, h being VECTOR of (ComplexVectSpace (X,Y))
for c being Complex holds
( h = c * f iff for x being Element of X holds h . x = c * (f . x) )
let Y be ComplexLinearSpace; ::_thesis: for f, h being VECTOR of (ComplexVectSpace (X,Y))
for c being Complex holds
( h = c * f iff for x being Element of X holds h . x = c * (f . x) )
let f, h be VECTOR of (ComplexVectSpace (X,Y)); ::_thesis: for c being Complex holds
( h = c * f iff for x being Element of X holds h . x = c * (f . x) )
let c be Complex; ::_thesis: ( h = c * f iff for x being Element of X holds h . x = c * (f . x) )
reconsider f9 = f, h9 = h as Element of Funcs (X, the carrier of Y) ;
hereby  ::_thesis: ( ( for x being Element of X holds h . x = c * (f . x) ) implies h = c * f )
assume A1: h = c * f ; ::_thesis: for x being Element of X holds h . x = c * (f . x)
let x be Element of X; ::_thesis: h . x = c * (f . x)
 h = (FuncExtMult (X,Y)) . [c,f9] by A1, CLVECT_1:def_1;
hence  h . x = c * (f . x) by Th2; ::_thesis: verum
end;
assume  for x being Element of X holds h . x = c * (f . x) ; ::_thesis: h = c * f
then  h9 = (FuncExtMult (X,Y)) . [c,f9] by Th2;
hence  h = c * f by CLVECT_1:def_1; ::_thesis: verum
end;

begin

definition
let X, Y be non empty CLSStruct ;
let IT be Function of X,Y;
attrIT is homogeneous  means :Def3: :: CLOPBAN1:def 3
 for x being VECTOR of X
for r being Complex holds IT . (r * x) = r * (IT . x);
end;

:: deftheorem Def3 defines homogeneous CLOPBAN1:def_3_:_
 for X, Y being non empty CLSStruct
for IT being Function of X,Y holds
( IT is homogeneous iff for x being VECTOR of X
for r being Complex holds IT . (r * x) = r * (IT . x) );

registration
let X be non empty CLSStruct ;
let Y be ComplexLinearSpace;
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 CLOPBAN1:def_3 ::_thesis: verum
let x be VECTOR of X; ::_thesis: for c being Complex holds f . (c * x) = c * (f . x)
let c be Complex; ::_thesis: f . (c * x) = c * (f . x)
thus f . (c * x) = 0. Y by FUNCOP_1:7
.= c * (0. Y) by CLVECT_1:1
.= c * (f . x) by FUNCOP_1:7 ; ::_thesis: verum
end;
end;
end;

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

definition
let X, Y be ComplexLinearSpace;
func LinearOperators (X,Y) ->  Subset of (ComplexVectSpace ( the carrier of X,Y)) means :Def4: :: CLOPBAN1:def 4
 for x being set holds
( x in it iff x is LinearOperator of X,Y );
existence
 ex b1 being Subset of (ComplexVectSpace ( 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 (ComplexVectSpace ( 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 (ComplexVectSpace ( 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 (ComplexVectSpace ( 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 (ComplexVectSpace ( 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 Def4 defines LinearOperators CLOPBAN1:def_4_:_
 for X, Y being ComplexLinearSpace
for b3 being Subset of (ComplexVectSpace ( 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 ComplexLinearSpace;
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);
A1: the carrier of X --> (0. Y) is homogeneous
proof
let x be VECTOR of X; :: according to CLOPBAN1:def_3 ::_thesis: for r being Complex holds ( the carrier of X --> (0. Y)) . (r * x) = r * (( the carrier of X --> (0. Y)) . x)
let c be Complex; ::_thesis: ( the carrier of X --> (0. Y)) . (c * x) = c * (( the carrier of X --> (0. Y)) . x)
thus ( the carrier of X --> (0. Y)) . (c * x) = 0. Y by FUNCOP_1:7
.= c * (0. Y) by CLVECT_1:1
.= c * (( the carrier of X --> (0. Y)) . x) by FUNCOP_1:7 ; ::_thesis: verum
end;
 the carrier of X --> (0. Y) is additive
proof
let x, y be VECTOR of X; :: according to VECTSP_1:def_20 ::_thesis: ( the carrier of X --> (0. Y)) . (x + y) = (( the carrier of X --> (0. Y)) . x) + (( the carrier of X --> (0. Y)) . y)
thus ( the carrier of X --> (0. Y)) . (x + y) = 0. Y by FUNCOP_1:7
.= (0. Y) + (0. Y) by RLVECT_1:4
.= (( the carrier of X --> (0. Y)) . x) + (0. Y) by FUNCOP_1:7
.= (( the carrier of X --> (0. Y)) . x) + (( the carrier of X --> (0. Y)) . y) by FUNCOP_1:7 ; ::_thesis: verum
end;
hence  not LinearOperators (X,Y) is empty by A1, Def4; ::_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 )
thus  ( not x in LinearOperators (X,Y) or x is set ) ; ::_thesis: verum
end;
end;

theorem Th13: :: CLOPBAN1:13
for X, Y being ComplexLinearSpace holds LinearOperators (X,Y) is linearly-closed
proof
let X, Y be ComplexLinearSpace; ::_thesis: LinearOperators (X,Y) is linearly-closed
set W = LinearOperators (X,Y);
A1: for c being Complex
for v being VECTOR of (ComplexVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds
c * v in LinearOperators (X,Y)
proof
let c be Complex; ::_thesis: for v being VECTOR of (ComplexVectSpace ( the carrier of X,Y)) st v in LinearOperators (X,Y) holds
c * v in LinearOperators (X,Y)
let v be VECTOR of (ComplexVectSpace ( the carrier of X,Y)); ::_thesis: ( v in LinearOperators (X,Y) implies c * v in LinearOperators (X,Y) )
assume A2: v in LinearOperators (X,Y) ; ::_thesis: c * v in LinearOperators (X,Y)
 c * v is LinearOperator of X,Y
proof
reconsider f = c * v as Function of X,Y by FUNCT_2:66;
A3: 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 CLOPBAN1:def_3 ::_thesis: for r being Complex holds f . (r * x) = r * (f . x)
let s be Complex; ::_thesis: f . (s * x) = s * (f . x)
A4: v9 is LinearOperator of X,Y by A2, Def4;
A5: f = (FuncExtMult ( the carrier of X,Y)) . [c,v9] by CLVECT_1:def_1;
hence f . (s * x) = c * (v9 . (s * x)) by Th2
.= c * (s * (v9 . x)) by A4, Def3
.= (c * s) * (v9 . x) by CLVECT_1:def_4
.= s * (c * (v9 . x)) by CLVECT_1:def_4
.= s * (f . x) by A5, 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)
A6: v9 is LinearOperator of X,Y by A2, Def4;
A7: f = (FuncExtMult ( the carrier of X,Y)) . [c,v9] by CLVECT_1:def_1;
hence f . (x + y) = c * (v9 . (x + y)) by Th2
.= c * ((v9 . x) + (v9 . y)) by A6, VECTSP_1:def_20
.= (c * (v9 . x)) + (c * (v9 . y)) by CLVECT_1:def_2
.= (f . x) + (c * (v9 . y)) by A7, Th2
.= (f . x) + (f . y) by A7, Th2 ;
::_thesis: verum
end;
hence  c * v is LinearOperator of X,Y by A3; ::_thesis: verum
end;
hence  c * v in LinearOperators (X,Y) by Def4; ::_thesis: verum
end;
 for v, u being VECTOR of (ComplexVectSpace ( 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 (ComplexVectSpace ( 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
A8: v in LinearOperators (X,Y) and
A9: 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;
A10: 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 CLOPBAN1:def_3 ::_thesis: for r being Complex holds f . (r * x) = r * (f . x)
let s be Complex; ::_thesis: f . (s * x) = s * (f . x)
A11: u9 is LinearOperator of X,Y by A9, Def4;
A12: v9 is LinearOperator of X,Y by A8, Def4;
thus f . (s * x) = (u9 . (s * x)) + (v9 . (s * x)) by LOPBAN_1:1
.= (s * (u9 . x)) + (v9 . (s * x)) by A11, Def3
.= (s * (u9 . x)) + (s * (v9 . x)) by A12, Def3
.= s * ((u9 . x) + (v9 . x)) by CLVECT_1:def_2
.= s * (f . x) by LOPBAN_1:1 ; ::_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)
A13: u9 is LinearOperator of X,Y by A9, Def4;
A14: v9 is LinearOperator of X,Y by A8, Def4;
thus f . (x + y) = (u9 . (x + y)) + (v9 . (x + y)) by LOPBAN_1:1
.= ((u9 . x) + (u9 . y)) + (v9 . (x + y)) by A13, VECTSP_1:def_20
.= ((u9 . x) + (u9 . y)) + ((v9 . x) + (v9 . y)) by A14, 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 LOPBAN_1:1
.= (f . x) + ((u9 . y) + (v9 . y)) by RLVECT_1:def_3
.= (f . x) + (f . y) by LOPBAN_1:1 ; ::_thesis: verum
end;
hence  v + u is LinearOperator of X,Y by A10; ::_thesis: verum
end;
hence  v + u in LinearOperators (X,Y) by Def4; ::_thesis: verum
end;
hence  LinearOperators (X,Y) is linearly-closed by A1, CLVECT_1:def_7; ::_thesis: verum
end;

theorem :: CLOPBAN1:14
for X, Y being ComplexLinearSpace holds CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is Subspace of ComplexVectSpace ( the carrier of X,Y) by Th13, CSSPACE:11;

registration
let X, Y be ComplexLinearSpace;
cluster CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is Abelian & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is add-associative & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is right_zeroed & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is right_complementable & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is vector-distributive & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is scalar-associative & CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is scalar-unital ) by Th13, CSSPACE:11;
end;

definition
let X, Y be ComplexLinearSpace;
func C_VectorSpace_of_LinearOperators (X,Y) ->  ComplexLinearSpace equals :: CLOPBAN1:def 5
 CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #);
coherence
 CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #) is ComplexLinearSpace ;
end;

:: deftheorem  defines C_VectorSpace_of_LinearOperators CLOPBAN1:def_5_:_
 for X, Y being ComplexLinearSpace holds C_VectorSpace_of_LinearOperators (X,Y) = CLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(ComplexVectSpace ( the carrier of X,Y)))) #);

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

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

definition
let X, Y be ComplexLinearSpace;
let f be Element of (C_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 Def4;
 f . v is VECTOR of Y ;
hence  f . v is VECTOR of Y ; ::_thesis: verum
end;
end;

theorem Th15: :: CLOPBAN1:15
for X, Y being ComplexLinearSpace
for f, g, h being VECTOR of (C_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 ComplexLinearSpace; ::_thesis: for f, g, h being VECTOR of (C_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 (C_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 Def4;
A1: C_VectorSpace_of_LinearOperators (X,Y) is Subspace of ComplexVectSpace ( the carrier of X,Y) by Th13, CSSPACE:11;
then reconsider f1 = f as VECTOR of (ComplexVectSpace ( the carrier of X,Y)) by CLVECT_1:29;
reconsider h1 = h as VECTOR of (ComplexVectSpace ( the carrier of X,Y)) by A1, CLVECT_1:29;
reconsider g1 = g as VECTOR of (ComplexVectSpace ( the carrier of X,Y)) by A1, CLVECT_1:29;
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, CLVECT_1:32;
hence  h9 . x = (f9 . x) + (g9 . x) by LOPBAN_1:1; ::_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 LOPBAN_1:1;
hence  h = f + g by A1, CLVECT_1:32; ::_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 Th16: :: CLOPBAN1:16
for X, Y being ComplexLinearSpace
for f, h being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y))
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
proof
let X, Y be ComplexLinearSpace; ::_thesis: for f, h being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y))
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
let f, h be VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)); ::_thesis: for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
reconsider f9 = f, h9 = h as LinearOperator of X,Y by Def4;
let c be Complex; ::_thesis: ( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
A1: C_VectorSpace_of_LinearOperators (X,Y) is Subspace of ComplexVectSpace ( the carrier of X,Y) by Th13, CSSPACE:11;
then reconsider f1 = f as VECTOR of (ComplexVectSpace ( the carrier of X,Y)) by CLVECT_1:29;
reconsider h1 = h as VECTOR of (ComplexVectSpace ( the carrier of X,Y)) by A1, CLVECT_1:29;
A2: now__::_thesis:_(_h_=_c_*_f_implies_for_x_being_Element_of_X_holds_h9_._x_=_c_*_(f9_._x)_)
assume A3: h = c * f ; ::_thesis: for x being Element of X holds h9 . x = c * (f9 . x)
let x be Element of X; ::_thesis: h9 . x = c * (f9 . x)
 h1 = c * f1 by A1, A3, CLVECT_1:33;
hence  h9 . x = c * (f9 . x) by Th12; ::_thesis: verum
end;
now__::_thesis:_(_(_for_x_being_Element_of_X_holds_h9_._x_=_c_*_(f9_._x)_)_implies_h_=_c_*_f_)
assume  for x being Element of X holds h9 . x = c * (f9 . x) ; ::_thesis: h = c * f
then  h1 = c * f1 by Th12;
hence  h = c * f by A1, CLVECT_1:33; ::_thesis: verum
end;
hence  ( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) ) by A2; ::_thesis: verum
end;

theorem Th17: :: CLOPBAN1:17
for X, Y being ComplexLinearSpace holds 0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)
proof
let X, Y be ComplexLinearSpace; ::_thesis: 0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)
A1: 0. (ComplexVectSpace ( the carrier of X,Y)) = the carrier of X --> (0. Y) by LOPBAN_1:def_3;
 C_VectorSpace_of_LinearOperators (X,Y) is Subspace of ComplexVectSpace ( the carrier of X,Y) by Th13, CSSPACE:11;
hence  0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, CLVECT_1:30; ::_thesis: verum
end;

theorem Th18: :: CLOPBAN1:18
for X, Y being ComplexLinearSpace holds the carrier of X --> (0. Y) is LinearOperator of X,Y
proof
let X, Y be ComplexLinearSpace; ::_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 CLOPBAN1:def_3 ::_thesis: for r being Complex holds f . (r * x) = r * (f . x)
let c be Complex; ::_thesis: f . (c * x) = c * (f . x)
thus f . (c * x) = 0. Y by FUNCOP_1:7
.= c * (0. Y) by CLVECT_1:1
.= c * (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 Th19: :: CLOPBAN1:19
for X being ComplexNormSpace
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 ComplexNormSpace; ::_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, CLVECT_1:def_16;
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 CLVECT_1:110;
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, CLVECT_1:117;
hence  ( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| ) by A3, SEQ_2:def_7; ::_thesis: verum
end;

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

:: deftheorem Def6 defines Lipschitzian CLOPBAN1:def_6_:_
 for X, Y being ComplexNormSpace
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 Th20: :: CLOPBAN1:20
for X, Y being ComplexNormSpace
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 ComplexNormSpace; ::_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.|| by CLVECT_1:102 ; ::_thesis: verum
end;
take  0 ; :: according to CLOPBAN1:def_6 ::_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 ComplexNormSpace;
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 Th18;
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 Th20; ::_thesis: verum
end;
end;

definition
let X, Y be ComplexNormSpace;
func BoundedLinearOperators (X,Y) ->  Subset of (C_VectorSpace_of_LinearOperators (X,Y)) means :Def7: :: CLOPBAN1:def 7
 for x being set holds
( x in it iff x is Lipschitzian LinearOperator of X,Y );
existence
 ex b1 being Subset of (C_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 (C_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 (C_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 Def4;
hence  x in IT by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of (C_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 (C_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 Def7 defines BoundedLinearOperators CLOPBAN1:def_7_:_
 for X, Y being ComplexNormSpace
for b3 being Subset of (C_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 ComplexNormSpace;
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 Th18;
 for x being VECTOR of X holds f . x = 0. Y by FUNCOP_1:7;
then  f is Lipschitzian by Th20;
hence  not BoundedLinearOperators (X,Y) is empty by Def7; ::_thesis: verum
end;
end;

theorem Th21: :: CLOPBAN1:21
for X, Y being ComplexNormSpace holds BoundedLinearOperators (X,Y) is linearly-closed
proof
let X, Y be ComplexNormSpace; ::_thesis: BoundedLinearOperators (X,Y) is linearly-closed
set W = BoundedLinearOperators (X,Y);
A1: for v, u being VECTOR of (C_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 (C_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 Def4;
 f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by A2, Def7;
consider K2 being Real such that
A4: 0 <= K2 and
A5: for x being VECTOR of X holds ||.(v1 . x).|| <= K2 * ||.x.|| by Def6;
reconsider u1 = u as Lipschitzian LinearOperator of X,Y by A3, Def7;
consider K1 being Real such that
A6: 0 <= K1 and
A7: for x being VECTOR of X holds ||.(u1 . x).|| <= K1 * ||.x.|| by Def6;
take K3 = K1 + K2; :: according to CLOPBAN1:def_6 ::_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 CLVECT_1:def_13;
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 Th15;
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 Def7; ::_thesis: verum
end;
 for c being Complex
for v being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) holds
c * v in BoundedLinearOperators (X,Y)
proof
let c be Complex; ::_thesis: for v being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) st v in BoundedLinearOperators (X,Y) holds
c * v in BoundedLinearOperators (X,Y)
let v be VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)); ::_thesis: ( v in BoundedLinearOperators (X,Y) implies c * v in BoundedLinearOperators (X,Y) )
assume A11: v in BoundedLinearOperators (X,Y) ; ::_thesis: c * v in BoundedLinearOperators (X,Y)
reconsider f = c * v as LinearOperator of X,Y by Def4;
 f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by A11, Def7;
consider K being Real such that
A12: 0 <= K and
A13: for x being VECTOR of X holds ||.(v1 . x).|| <= K * ||.x.|| by Def6;
take  |.c.| * K ; :: according to CLOPBAN1:def_6 ::_thesis: ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ||.x.|| ) )
A14: now__::_thesis:_for_x_being_VECTOR_of_X_holds_||.(f_._x).||_<=_(|.c.|_*_K)_*_||.x.||
let x be VECTOR of X; ::_thesis: ||.(f . x).|| <= (|.c.| * K) * ||.x.||
 0 <= |.c.| by COMPLEX1:46;
then A15: |.c.| * ||.(v1 . x).|| <= |.c.| * (K * ||.x.||) by A13, XREAL_1:64;
 ||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| by CLVECT_1:def_13;
hence  ||.(f . x).|| <= (|.c.| * K) * ||.x.|| by A15, Th16; ::_thesis: verum
end;
 0 <= |.c.| by COMPLEX1:46;
hence  ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ||.x.|| ) ) by A12, A14; ::_thesis: verum
end;
hence  c * v in BoundedLinearOperators (X,Y) by Def7; ::_thesis: verum
end;
hence  BoundedLinearOperators (X,Y) is linearly-closed by A1, CLVECT_1:def_7; ::_thesis: verum
end;

theorem :: CLOPBAN1:22
for X, Y being ComplexNormSpace holds CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is Subspace of C_VectorSpace_of_LinearOperators (X,Y) by Th21, CSSPACE:11;

registration
let X, Y be ComplexNormSpace;
cluster CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital ) by Th21, CSSPACE:11;
end;

definition
let X, Y be ComplexNormSpace;
func C_VectorSpace_of_BoundedLinearOperators (X,Y) ->  ComplexLinearSpace equals :: CLOPBAN1:def 8
 CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #);
coherence
 CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is ComplexLinearSpace ;
end;

:: deftheorem  defines C_VectorSpace_of_BoundedLinearOperators CLOPBAN1:def_8_:_
 for X, Y being ComplexNormSpace holds C_VectorSpace_of_BoundedLinearOperators (X,Y) = CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #);

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

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

definition
let X, Y be ComplexNormSpace;
let f be Element of (C_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 Def7;
 f . v is VECTOR of Y ;
hence  f . v is VECTOR of Y ; ::_thesis: verum
end;
end;

theorem Th23: :: CLOPBAN1:23
for X, Y being ComplexNormSpace
for f, g, h being VECTOR of (C_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 ComplexNormSpace; ::_thesis: for f, g, h being VECTOR of (C_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 (C_VectorSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
A1: C_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of C_VectorSpace_of_LinearOperators (X,Y) by Th21, CSSPACE:11;
then reconsider f1 = f as VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) by CLVECT_1:29;
reconsider h1 = h as VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) by A1, CLVECT_1:29;
reconsider g1 = g as VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) by A1, CLVECT_1:29;
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, CLVECT_1:32;
hence  h . x = (f . x) + (g . x) by Th15; ::_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 Th15;
hence  h = f + g by A1, CLVECT_1:32; ::_thesis: verum
end;

theorem Th24: :: CLOPBAN1:24
for X, Y being ComplexNormSpace
for f, h being VECTOR of (C_VectorSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
proof
let X, Y be ComplexNormSpace; ::_thesis: for f, h being VECTOR of (C_VectorSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
let f, h be VECTOR of (C_VectorSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
let c be Complex; ::_thesis: ( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
A1: C_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of C_VectorSpace_of_LinearOperators (X,Y) by Th21, CSSPACE:11;
then reconsider f1 = f as VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) by CLVECT_1:29;
reconsider h1 = h as VECTOR of (C_VectorSpace_of_LinearOperators (X,Y)) by A1, CLVECT_1:29;
hereby  ::_thesis: ( ( for x being VECTOR of X holds h . x = c * (f . x) ) implies h = c * f )
assume A2: h = c * f ; ::_thesis: for x being Element of X holds h . x = c * (f . x)
let x be Element of X; ::_thesis: h . x = c * (f . x)
 h1 = c * f1 by A1, A2, CLVECT_1:33;
hence  h . x = c * (f . x) by Th16; ::_thesis: verum
end;
assume  for x being Element of X holds h . x = c * (f . x) ; ::_thesis: h = c * f
then  h1 = c * f1 by Th16;
hence  h = c * f by A1, CLVECT_1:33; ::_thesis: verum
end;

theorem Th25: :: CLOPBAN1:25
for X, Y being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y)
proof
let X, Y be ComplexNormSpace; ::_thesis: 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y)
A1: 0. (C_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y) by Th17;
 C_VectorSpace_of_BoundedLinearOperators (X,Y) is Subspace of C_VectorSpace_of_LinearOperators (X,Y) by Th21, CSSPACE:11;
hence  0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y) by A1, CLVECT_1:30; ::_thesis: verum
end;

definition
let X, Y be ComplexNormSpace;
let f be set ;
assume A1: f in BoundedLinearOperators (X,Y) ;
func modetrans (f,X,Y) ->  Lipschitzian LinearOperator of X,Y equals :Def9: :: CLOPBAN1:def 9
f;
coherence
 f is Lipschitzian LinearOperator of X,Y by A1, Def7;
end;

:: deftheorem Def9 defines modetrans CLOPBAN1:def_9_:_
 for X, Y being ComplexNormSpace
for f being set st f in BoundedLinearOperators (X,Y) holds
modetrans (f,X,Y) = f;

definition
let X, Y be ComplexNormSpace;
let u be LinearOperator of X,Y;
func PreNorms u ->  non empty Subset of REAL equals :: CLOPBAN1:def 10
 {  ||.(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 by CLVECT_1:102;
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 CLOPBAN1:def_10_:_
 for X, Y being ComplexNormSpace
for u being LinearOperator of X,Y holds PreNorms u =  {  ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  ;

theorem Th26: :: CLOPBAN1:26
for X, Y being ComplexNormSpace
for g being Lipschitzian LinearOperator of X,Y holds PreNorms g is bounded_above
proof
let X, Y be ComplexNormSpace; ::_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 Def6;
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 :: CLOPBAN1:27
for X, Y being ComplexNormSpace
for g being LinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )
proof
let X, Y be ComplexNormSpace; ::_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 by NORMSP_0:def_6;
g . t = g . (0c * (0. X)) by A3, CLVECT_1:1
.= 0c * (g . (0. X)) by Def3
.= 0. Y by CLVECT_1:1 ;
hence  ||.(g . t).|| <= K * ||.t.|| by A4, NORMSP_0:def_6; ::_thesis: verum
end;
caseA5: t <> 0. X ; ::_thesis: ||.(g . t).|| <= K * ||.t.||
reconsider t0 = (||.t.|| ") + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def_2;
reconsider t1 = t0 * t as VECTOR of X ;
A6: ||.t.|| <> 0 by A5, NORMSP_0:def_5;
then A7: ||.t.|| > 0 by CLVECT_1:105;
A8: |.((||.t.|| ") + (0 * <i>)).| = abs (1 * (||.t.|| "))
.= abs (1 / ||.t.||) by XCMPLX_0:def_9
.= 1 / (abs ||.t.||) by ABSVALUE:7
.= 1 / ||.t.|| by A7, ABSVALUE:def_1
.= 1 * (||.t.|| ") by XCMPLX_0:def_9
.= ||.t.|| " ;
then A9: ||.(g . t).|| / ||.t.|| = ||.(g . t).|| * |.t0.| by XCMPLX_0:def_9
.= ||.(t0 * (g . t)).|| by CLVECT_1:def_13
.= ||.(g . t1).|| by Def3 ;
||.t1.|| = |.t0.| * ||.t.|| by CLVECT_1:def_13
.= 1 by A6, A8, XCMPLX_0:def_7 ;
then  ||.(g . t).|| / ||.t.|| in PreNorms g by A9;
then A10: ||.(g . t).|| / ||.t.|| <= K by A1, SEQ_4:def_1;
(||.(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).|| <= K * ||.t.|| by A7, A10, 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
A11: r0 in PreNorms g by XBOOLE_0:def_1;
reconsider r0 = r0 as Real by A11;
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 by CLVECT_1:105; ::_thesis: verum
end;
then  0 <= r0 by A11;
hence  0 <= K by A1, A11, SEQ_4:def_1; ::_thesis: verum
end;
hence  g is Lipschitzian by A2, Def6; ::_thesis: verum
end;
hence  ( g is Lipschitzian iff PreNorms g is bounded_above ) by Th26; ::_thesis: verum
end;

definition
let X, Y be ComplexNormSpace;
func BoundedLinearOperatorsNorm (X,Y) ->  Function of (BoundedLinearOperators (X,Y)),REAL means :Def11: :: CLOPBAN1:def 11
 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 ;
 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);
hence  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))) ; ::_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 Def11 defines BoundedLinearOperatorsNorm CLOPBAN1:def_11_:_
 for X, Y being ComplexNormSpace
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 Th28: :: CLOPBAN1:28
for X, Y being ComplexNormSpace
for f being Lipschitzian LinearOperator of X,Y holds modetrans (f,X,Y) = f
proof
let X, Y be ComplexNormSpace; ::_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 Def7;
hence  modetrans (f,X,Y) = f by Def9; ::_thesis: verum
end;

theorem Th29: :: CLOPBAN1:29
for X, Y being ComplexNormSpace
for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
proof
let X, Y be ComplexNormSpace; ::_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 Def7;
hence (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms (modetrans (f9,X,Y))) by Def11
.= upper_bound (PreNorms f) by Th28 ;
::_thesis: verum
end;

definition
let X, Y be ComplexNormSpace;
func C_NormSpace_of_BoundedLinearOperators (X,Y) ->  non empty CNORMSTR  equals :: CLOPBAN1:def 12
 CNORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);
coherence
 CNORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty CNORMSTR ;
end;

:: deftheorem  defines C_NormSpace_of_BoundedLinearOperators CLOPBAN1:def_12_:_
 for X, Y being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) = CNORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);

theorem Th30: :: CLOPBAN1:30
for X, Y being ComplexNormSpace holds the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y))
proof
let X, Y be ComplexNormSpace; ::_thesis: the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y))
the carrier of X --> (0. Y) = 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) by Th25
.= 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ;
hence  the carrier of X --> (0. Y) = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ; ::_thesis: verum
end;

theorem Th31: :: CLOPBAN1:31
for X, Y being ComplexNormSpace
for f being Point of (C_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 ComplexNormSpace; ::_thesis: for f being Point of (C_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 (C_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 Th26;
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 by NORMSP_0:def_6;
g . t = g . (0c * (0. X)) by A3, CLVECT_1:1
.= 0c * (g . (0. X)) by Def3
.= 0. Y by CLVECT_1:1 ;
hence  ||.(g . t).|| <= ||.f.|| * ||.t.|| by A4, NORMSP_0:def_6; ::_thesis: verum
end;
caseA5: t <> 0. X ; ::_thesis: ||.(g . t).|| <= ||.f.|| * ||.t.||
reconsider t0 = (||.t.|| ") + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def_2;
reconsider t1 = t0 * t as VECTOR of X ;
A6: ||.t.|| <> 0 by A5, NORMSP_0:def_5;
then A7: ||.t.|| > 0 by CLVECT_1:105;
A8: |.t0.| = abs (1 * (||.t.|| "))
.= abs (1 / ||.t.||) by XCMPLX_0:def_9
.= 1 / (abs ||.t.||) by ABSVALUE:7
.= 1 / ||.t.|| by A7, ABSVALUE:def_1
.= 1 * (||.t.|| ") by XCMPLX_0:def_9
.= ||.t.|| " ;
then A9: ||.(g . t).|| / ||.t.|| = ||.(g . t).|| * |.t0.| by XCMPLX_0:def_9
.= ||.(t0 * (g . t)).|| by CLVECT_1:def_13
.= ||.(g . t1).|| by Def3 ;
||.t1.|| = |.t0.| * ||.t.|| by CLVECT_1:def_13
.= 1 by A6, A8, XCMPLX_0:def_7 ;
then  ||.(g . t).|| / ||.t.|| in  {  ||.(g . s).|| where s is VECTOR of X : ||.s.|| <= 1  }  by A9;
then  ||.(g . t).|| / ||.t.|| <= upper_bound (PreNorms g) by A2, SEQ_4:def_1;
then  ||.(g . t).|| / ||.t.|| <= (BoundedLinearOperatorsNorm (X,Y)) . g by Th29;
then A10: ||.(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 A7, A10, 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 Th32: :: CLOPBAN1:32
for X, Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||
proof
let X, Y be ComplexNormSpace; ::_thesis: for f being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||
let f be Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: 0 <= ||.f.||
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def7;
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 Th26;
A3: (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms g) by Th29;
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 by CLVECT_1:105; ::_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 Th33: :: CLOPBAN1:33
for X, Y being ComplexNormSpace
for f being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) holds
0 = ||.f.||
proof
let X, Y be ComplexNormSpace; ::_thesis: for f being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) holds
0 = ||.f.||
let f be Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: ( f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies 0 = ||.f.|| )
assume A1: f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ; ::_thesis: 0 = ||.f.||
thus  ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def7;
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 Th26;
A5: z = g by A1, Th30;
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 by NORMSP_0:def_6 ;
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 Th29;
hence  ||.f.|| = 0 ; ::_thesis: verum
end;
end;

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

definition
let X, Y be ComplexNormSpace;
let f be Element of (C_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 Def7;
 f . v is VECTOR of Y ;
hence  f . v is VECTOR of Y ; ::_thesis: verum
end;
end;

theorem Th34: :: CLOPBAN1:34
for X, Y being ComplexNormSpace
for f, g, h being Point of (C_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 ComplexNormSpace; ::_thesis: for f, g, h being Point of (C_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 (C_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 (C_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 Th23; ::_thesis: verum
end;

theorem Th35: :: CLOPBAN1:35
for X, Y being ComplexNormSpace
for f, h being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
proof
let X, Y be ComplexNormSpace; ::_thesis: for f, h being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
let f, h be Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
let c be Complex; ::_thesis: ( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )
reconsider f1 = f as VECTOR of (C_VectorSpace_of_BoundedLinearOperators (X,Y)) ;
reconsider h1 = h as VECTOR of (C_VectorSpace_of_BoundedLinearOperators (X,Y)) ;
A1: now__::_thesis:_(_h1_=_c_*_f1_implies_h_=_c_*_f_)
assume  h1 = c * f1 ; ::_thesis: h = c * f
hence h = (Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) . [c,f1] by CLVECT_1:def_1
.= c * f by CLVECT_1:def_1 ;
::_thesis: verum
end;
now__::_thesis:_(_h_=_c_*_f_implies_h1_=_c_*_f1_)
assume  h = c * f ; ::_thesis: h1 = c * f1
hence h1 = (Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) . [c,f] by CLVECT_1:def_1
.= c * f1 by CLVECT_1:def_1 ;
::_thesis: verum
end;
hence  ( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) ) by A1, Th24; ::_thesis: verum
end;

theorem Th36: :: CLOPBAN1:36
for X, Y being ComplexNormSpace
for f, g being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof
let X, Y be ComplexNormSpace; ::_thesis: for f, g being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let f, g be Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)); ::_thesis: for c being Complex holds
( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
let c be Complex; ::_thesis: ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
A1: now__::_thesis:_(_f_=_0._(C_NormSpace_of_BoundedLinearOperators_(X,Y))_implies_||.f.||_=_0_)
assume A2: f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ; ::_thesis: ||.f.|| = 0
thus  ||.f.|| = 0 ::_thesis: verum
proof
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def7;
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 Th26;
A6: z = g by A2, Th30;
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 by NORMSP_0:def_6 ;
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 Th29;
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 Def7;
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 Th32;
then A13: ||.g.|| * ||.t.|| <= ||.g.|| * 1 by A12, XREAL_1:64;
 0 <= ||.f.|| by Th32;
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 CLVECT_1:def_13;
A16: ||.(g1 . t).|| <= ||.g.|| * ||.t.|| by Th31;
 ||.(f1 . t).|| <= ||.f.|| * ||.t.|| by Th31;
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 Th34;
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 Th29;
hence  ||.(f + g).|| <= ||.f.|| + ||.g.|| by A18, A10; ::_thesis: verum
end;
A19: ||.(c * f).|| = |.c.| * ||.f.||
proof
reconsider f1 = f, h1 = c * f as Lipschitzian LinearOperator of X,Y by Def7;
A20: ( ( for s being real number st s in PreNorms h1 holds
s <= |.c.| * ||.f.|| ) implies upper_bound (PreNorms h1) <= |.c.| * ||.f.|| ) by SEQ_4:45;
A21: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.(h1_._t).||_<=_|.c.|_*_||.f.||
A22: 0 <= ||.f.|| by Th32;
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.(h1 . t).|| <= |.c.| * ||.f.|| )
assume  ||.t.|| <= 1 ; ::_thesis: ||.(h1 . t).|| <= |.c.| * ||.f.||
then A23: ||.f.|| * ||.t.|| <= ||.f.|| * 1 by A22, XREAL_1:64;
 ||.(f1 . t).|| <= ||.f.|| * ||.t.|| by Th31;
then A24: ||.(f1 . t).|| <= ||.f.|| by A23, XXREAL_0:2;
A25: ||.(c * (f1 . t)).|| = |.c.| * ||.(f1 . t).|| by CLVECT_1:def_13;
A26: 0 <= |.c.| by COMPLEX1:46;
 ||.(h1 . t).|| = ||.(c * (f1 . t)).|| by Th35;
hence  ||.(h1 . t).|| <= |.c.| * ||.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_<=_|.c.|_*_||.f.||
let r be Real; ::_thesis: ( r in PreNorms h1 implies r <= |.c.| * ||.f.|| )
assume  r in PreNorms h1 ; ::_thesis: r <= |.c.| * ||.f.||
then  ex t being VECTOR of X st
( r = ||.(h1 . t).|| & ||.t.|| <= 1 ) ;
hence  r <= |.c.| * ||.f.|| by A21; ::_thesis: verum
end;
A28: now__::_thesis:_(_(_c_<>_0c_&_|.c.|_*_||.f.||_<=_||.(c_*_f).||_)_or_(_c_=_0c_&_||.(c_*_f).||_=_|.c.|_*_||.f.||_)_)
percases ( c <> 0c or c = 0c ) ;
caseA29: c <> 0c ; ::_thesis: |.c.| * ||.f.|| <= ||.(c * f).||
A30: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.(f1_._t).||_<=_(|.c.|_")_*_||.(c_*_f).||
A31: 0 <= ||.(c * f).|| by Th32;
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.(f1 . t).|| <= (|.c.| ") * ||.(c * f).|| )
assume  ||.t.|| <= 1 ; ::_thesis: ||.(f1 . t).|| <= (|.c.| ") * ||.(c * f).||
then A32: ||.(c * f).|| * ||.t.|| <= ||.(c * f).|| * 1 by A31, XREAL_1:64;
 ||.(h1 . t).|| <= ||.(c * f).|| * ||.t.|| by Th31;
then A33: ||.(h1 . t).|| <= ||.(c * f).|| by A32, XXREAL_0:2;
 h1 . t = c * (f1 . t) by Th35;
then A34: (c ") * (h1 . t) = ((c ") * c) * (f1 . t) by CLVECT_1:def_4
.= 1r * (f1 . t) by A29, COMPLEX1:def_4, XCMPLX_0:def_7
.= f1 . t by CLVECT_1:def_5 ;
A35: |.(c ").| = |.c.| " by COMPLEX1:66;
A36: 0 <= |.(c ").| by COMPLEX1:46;
 ||.((c ") * (h1 . t)).|| = |.(c ").| * ||.(h1 . t).|| by CLVECT_1:def_13;
hence  ||.(f1 . t).|| <= (|.c.| ") * ||.(c * 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_<=_(|.c.|_")_*_||.(c_*_f).||
let r be Real; ::_thesis: ( r in PreNorms f1 implies r <= (|.c.| ") * ||.(c * f).|| )
assume  r in PreNorms f1 ; ::_thesis: r <= (|.c.| ") * ||.(c * f).||
then  ex t being VECTOR of X st
( r = ||.(f1 . t).|| & ||.t.|| <= 1 ) ;
hence  r <= (|.c.| ") * ||.(c * f).|| by A30; ::_thesis: verum
end;
A38: ( ( for s being real number st s in PreNorms f1 holds
s <= (|.c.| ") * ||.(c * f).|| ) implies upper_bound (PreNorms f1) <= (|.c.| ") * ||.(c * f).|| ) by SEQ_4:45;
A39: 0 <= |.c.| by COMPLEX1:46;
 (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f1) by Th29;
then  ||.f.|| <= (|.c.| ") * ||.(c * f).|| by A37, A38;
then  |.c.| * ||.f.|| <= |.c.| * ((|.c.| ") * ||.(c * f).||) by A39, XREAL_1:64;
then A40: |.c.| * ||.f.|| <= (|.c.| * (|.c.| ")) * ||.(c * f).|| ;
 |.c.| <> 0 by A29, COMPLEX1:47;
then  |.c.| * ||.f.|| <= 1 * ||.(c * f).|| by A40, XCMPLX_0:def_7;
hence  |.c.| * ||.f.|| <= ||.(c * f).|| ; ::_thesis: verum
end;
caseA41: c = 0c ; ::_thesis: ||.(c * f).|| = |.c.| * ||.f.||
reconsider fz = f as VECTOR of (C_VectorSpace_of_BoundedLinearOperators (X,Y)) ;
c * f = (Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) . [c,f] by CLVECT_1:def_1
.= c * fz by CLVECT_1:def_1
.= 0. (C_VectorSpace_of_BoundedLinearOperators (X,Y)) by A41, CLVECT_1:1
.= 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ;
hence  ||.(c * f).|| = |.c.| * ||.f.|| by A41, Th33, COMPLEX1:44; ::_thesis: verum
end;
end;
end;
 (BoundedLinearOperatorsNorm (X,Y)) . (c * f) = upper_bound (PreNorms h1) by Th29;
then  ||.(c * f).|| <= |.c.| * ||.f.|| by A27, A20;
hence  ||.(c * f).|| = |.c.| * ||.f.|| by A28, XXREAL_0:1; ::_thesis: verum
end;
now__::_thesis:_(_||.f.||_=_0_implies_f_=_0._(C_NormSpace_of_BoundedLinearOperators_(X,Y))_)
reconsider g = f as Lipschitzian LinearOperator of X,Y by Def7;
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 A42: ||.f.|| = 0 ; ::_thesis: f = 0. (C_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 Th31;
then  ||.(g . t).|| = 0 by A42, CLVECT_1:105;
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. (C_NormSpace_of_BoundedLinearOperators (X,Y)) by Th30; ::_thesis: verum
end;
hence  ( ( ||.f.|| = 0 implies f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(c * f).|| = |.c.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| ) by A1, A19, A9; ::_thesis: verum
end;

theorem Th37: :: CLOPBAN1:37
for X, Y being ComplexNormSpace holds
( C_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like )
proof
let X, Y be ComplexNormSpace; ::_thesis: ( C_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like )
thus  C_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive ::_thesis: ( C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like )
proof
thus  ||.(0. (C_NormSpace_of_BoundedLinearOperators (X,Y))).|| = 0 by Th36; :: according to NORMSP_0:def_6 ::_thesis: verum
end;
 for x, y being Point of (C_NormSpace_of_BoundedLinearOperators (X,Y))
for c being Complex holds
( ( ||.x.|| = 0 implies x = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( x = 0. (C_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.x.|| = 0 ) & ||.(c * x).|| = |.c.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) by Th36;
hence  ( C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like ) by CLVECT_1:def_13, NORMSP_0:def_5; ::_thesis: verum
end;

theorem Th38: :: CLOPBAN1:38
for X, Y being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace
proof
let X, Y be ComplexNormSpace; ::_thesis: C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace
 CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is ComplexLinearSpace ;
hence  C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace by Th37, CSSPACE3:2; ::_thesis: verum
end;

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

theorem Th39: :: CLOPBAN1:39
for X, Y being ComplexNormSpace
for f, g, h being Point of (C_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 ComplexNormSpace; ::_thesis: for f, g, h being Point of (C_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 (C_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 Def7;
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. (C_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, Th34;
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 Th34;
then  f - g = h + (g - g) by RLVECT_1:def_3;
then  f - g = h + (0. (C_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 ComplexNormSpace;
attrX is complete  means :Def13: :: CLOPBAN1:def 13
 for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent ;
end;

:: deftheorem Def13 defines complete CLOPBAN1:def_13_:_
 for X being ComplexNormSpace 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 right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete for CNORMSTR ;
existence
 ex b1 being ComplexNormSpace st b1 is complete
proof
take  Complex_l1_Space ; ::_thesis: Complex_l1_Space is complete
thus  Complex_l1_Space is complete by Def13, CSSPACE3:9; ::_thesis: verum
end;
end;

definition
mode ComplexBanachSpace is complete ComplexNormSpace;
end;

Lm2:  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 Th40: :: CLOPBAN1:40
for X being ComplexNormSpace
for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )
proof
let X be ComplexNormSpace; ::_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, CLVECT_1:def_16;
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 CLVECT_1:110;
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 Th41: :: CLOPBAN1:41
for X, Y being ComplexNormSpace st Y is complete holds
for seq being sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof
let X, Y be ComplexNormSpace; ::_thesis: ( Y is complete implies for seq being sequence of (C_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 (C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (C_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 Def7;
A6: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A4;
 vseq . m is Lipschitzian LinearOperator of X,Y by Def7;
then A7: modetrans ((vseq . m),X,Y) = vseq . m by Th28;
 vseq . k is Lipschitzian LinearOperator of X,Y by Def7;
then A8: modetrans ((vseq . k),X,Y) = vseq . k by Th28;
 xseq . m = (modetrans ((vseq . m),X,Y)) . x by A4;
then  (xseq . m) - (xseq . k) = h1 . x by A7, A8, A6, Th39;
hence  ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th31; ::_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)) . (0c * x) by A10, CLVECT_1:1
.= 0c * ((modetrans ((vseq . m),X,Y)) . x) by Def3
.= 0. Y by CLVECT_1:1 ;
xseq . n = (modetrans ((vseq . n),X,Y)) . x by A4
.= (modetrans ((vseq . n),X,Y)) . (0c * x) by A10, CLVECT_1:1
.= 0c * ((modetrans ((vseq . n),X,Y)) . x) by Def3
.= 0. Y by CLVECT_1:1 ;
then ||.((xseq . n) - (xseq . m)).|| = ||.(0. Y).|| by A11, RLVECT_1:13
.= 0 by NORMSP_0:def_6 ;
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 by CLVECT_1:105;
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, A9, CSSPACE3: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 CSSPACE3:8;
then  xseq is convergent by A1, Def13;
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, CLVECT_1:119; ::_thesis: verum
end;
now__::_thesis:_for_x_being_VECTOR_of_X
for_c_being_Complex_holds_tseq_._(c_*_x)_=_c_*_(tseq_._x)
let x be VECTOR of X; ::_thesis: for c being Complex holds tseq . (c * x) = c * (tseq . x)
let c be Complex; ::_thesis: tseq . (c * x) = c * (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)) . (c * x) and
 zseq is convergent and
A33: tseq . (c * x) = lim zseq by A19;
now__::_thesis:_for_n_being_Element_of_NAT_holds_zseq_._n_=_c_*_(xseq_._n)
let n be Element of NAT ; ::_thesis: zseq . n = c * (xseq . n)
thus zseq . n = (modetrans ((vseq . n),X,Y)) . (c * x) by A32
.= c * ((modetrans ((vseq . n),X,Y)) . x) by Def3
.= c * (xseq . n) by A29 ; ::_thesis: verum
end;
then  zseq = c * xseq by CLVECT_1:def_14;
hence  tseq . (c * x) = c * (tseq . x) by A30, A31, A33, CLVECT_1:122; ::_thesis: verum
end;
then reconsider tseq = tseq as LinearOperator of X,Y by A20, Def3, 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, CSSPACE3: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 CLVECT_1:110;
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 CLOPBAN1:def_6 ::_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, Th19;
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 Def7;
hence  ||.(xseq . m).|| <= ||.(vseq . m).|| * ||.x.|| by A47, Th28, Th31; ::_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, Th19;
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 by CLVECT_1:105;
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, CSSPACE3: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 Def7;
A60: xseq . k = (modetrans ((vseq . k),X,Y)) . x by A56;
 vseq . m is Lipschitzian LinearOperator of X,Y by Def7;
then A61: modetrans ((vseq . m),X,Y) = vseq . m by Th28;
 vseq . k is Lipschitzian LinearOperator of X,Y by Def7;
then A62: modetrans ((vseq . k),X,Y) = vseq . k by Th28;
 xseq . m = (modetrans ((vseq . m),X,Y)) . x by A56;
then  (xseq . m) - (xseq . k) = h1 . x by A61, A62, A60, Th39;
hence  ||.((xseq . m) - (xseq . k)).|| <= ||.((vseq . m) - (vseq . k)).|| * ||.x.|| by Th31; ::_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;
 0 <= ||.x.|| by CLVECT_1:105;
then  ||.((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, CLVECT_1:115;
 lim (xseq - (xseq . n)) = (tseq . x) - (xseq . n) by A57, A58, CLVECT_1:121;
then A69: lim rseq = ||.((tseq . x) - (xseq . n)).|| by A68, A67, Th40;
 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 CLVECT_1:108 ;
hence  rseq . m <= e * ||.x.|| by A63, A70; ::_thesis: verum
end;
then  lim rseq <= e * ||.x.|| by A68, A67, Lm2, Th40;
hence  ||.((xseq . n) - (tseq . x)).|| <= e * ||.x.|| by A69, CLVECT_1:108; ::_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 (C_NormSpace_of_BoundedLinearOperators (X,Y)) by Def7;
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 Def7;
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 Def7;
then  modetrans ((vseq . n),X,Y) = vseq . n by Th28;
then  ||.(h1 . t).|| = ||.(((modetrans ((vseq . n),X,Y)) . t) - (tseq . t)).|| by Th39;
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 Th29;
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;
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 CLVECT_1:def_15; ::_thesis: verum
end;

theorem Th42: :: CLOPBAN1:42
for X being ComplexNormSpace
for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace
proof
let X be ComplexNormSpace; ::_thesis: for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace
let Y be ComplexBanachSpace; ::_thesis: C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace
 for seq being sequence of (C_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th41;
hence  C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace by Def13; ::_thesis: verum
end;

registration
let X be ComplexNormSpace;
let Y be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedLinearOperators (X,Y) ->  non empty complete ;
coherence
 C_NormSpace_of_BoundedLinearOperators (X,Y) is complete by Th42;
end;