let X, Y, Z be RealNormSpace; :: thesis: ex I being LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) )

set XC = the carrier of X;

set YC = the carrier of Y;

set ZC = the carrier of Z;

consider I0 being Function of (Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))),(Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z)) such that

A1: ( I0 is bijective & ( for f being Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))

for d, e being object st d in the carrier of X & e in the carrier of Y holds

(I0 . f) . (d,e) = (f . d) . e ) ) by NDIFF_6:1;

set LXYZ = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z))));

set BXYZ = the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));

set LYZ = the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z));

A3: the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) c= Funcs ( the carrier of Y, the carrier of Z) by XBOOLE_1:1;

A4: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) c= Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))) by XBOOLE_1:1;

Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))) c= Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))

then reconsider I = I0 | the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) as Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z)) by FUNCT_2:32;

A8: for x being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ( for p being Point of X

for q being Point of Y ex G being Lipschitzian LinearOperator of Y,Z st

( G = x . p & (I . x) . (p,q) = G . q ) ) & I . x is Lipschitzian BilinearOperator of X,Y,Z & I . x in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . x & ||.x.|| = ||.Ix.|| ) )

then reconsider I = I as Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))), the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by FUNCT_2:6;

A47: for x1, x2 being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds I . (x1 + x2) = (I . x1) + (I . x2)

for a being Real holds I . (a * x) = a * (I . x)

A55: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) )

ex x being object st

( x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . x )

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds ||.(I . u).|| <= 1 * ||.u.|| by A55;

then reconsider I = I as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by LOPBAN_1:def 8;

take I ; :: thesis: ( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) )

( I is one-to-one & I is onto ) by A1, A85, FUNCT_1:52, FUNCT_2:def 3;

hence ( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) ) by A55; :: thesis: verum

( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) )

set XC = the carrier of X;

set YC = the carrier of Y;

set ZC = the carrier of Z;

consider I0 being Function of (Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))),(Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z)) such that

A1: ( I0 is bijective & ( for f being Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))

for d, e being object st d in the carrier of X & e in the carrier of Y holds

(I0 . f) . (d,e) = (f . d) . e ) ) by NDIFF_6:1;

set LXYZ = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z))));

set BXYZ = the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));

set LYZ = the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z));

A3: the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) c= Funcs ( the carrier of Y, the carrier of Z) by XBOOLE_1:1;

A4: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) c= Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))) by XBOOLE_1:1;

Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))) c= Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))

proof

then A7:
the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) c= Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))
by A4, XBOOLE_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))) or x in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) )

assume x in Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))) ; :: thesis: x in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))

then consider f being Function such that

A6: ( x = f & dom f = the carrier of X & rng f c= the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) ) by FUNCT_2:def 2;

rng f c= Funcs ( the carrier of Y, the carrier of Z) by A3, A6, XBOOLE_1:1;

hence x in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by A6, FUNCT_2:def 2; :: thesis: verum

end;assume x in Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))) ; :: thesis: x in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))

then consider f being Function such that

A6: ( x = f & dom f = the carrier of X & rng f c= the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) ) by FUNCT_2:def 2;

rng f c= Funcs ( the carrier of Y, the carrier of Z) by A3, A6, XBOOLE_1:1;

hence x in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by A6, FUNCT_2:def 2; :: thesis: verum

then reconsider I = I0 | the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) as Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z)) by FUNCT_2:32;

A8: for x being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ( for p being Point of X

for q being Point of Y ex G being Lipschitzian LinearOperator of Y,Z st

( G = x . p & (I . x) . (p,q) = G . q ) ) & I . x is Lipschitzian BilinearOperator of X,Y,Z & I . x in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . x & ||.x.|| = ||.Ix.|| ) )

proof

then
rng I c= the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
by FUNCT_2:114;
let f be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))); :: thesis: ( ( for p being Point of X

for q being Point of Y ex G being Lipschitzian LinearOperator of Y,Z st

( G = f . p & (I . f) . (p,q) = G . q ) ) & I . f is Lipschitzian BilinearOperator of X,Y,Z & I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| ) )

A9: I . f = I0 . f by FUNCT_1:49;

A10: f in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by A7, TARSKI:def 3;

A11: f is Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by A7, TARSKI:def 3, FUNCT_2:66;

reconsider g = f as Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by A7, TARSKI:def 3, FUNCT_2:66;

reconsider F = f as Lipschitzian LinearOperator of X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def 9;

thus for x being Point of X

for y being Point of Y ex G being Lipschitzian LinearOperator of Y,Z st

( G = f . x & (I . f) . (x,y) = G . y ) :: thesis: ( I . f is Lipschitzian BilinearOperator of X,Y,Z & I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| ) )

A15: for x1, x2 being Point of X

for y being Point of Y holds BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y))

for y being Point of Y

for a being Real holds BL . ((a * x),y) = a * (BL . (x,y))

for y1, y2 being Point of Y holds BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2))

for y being Point of Y

for a being Real holds BL . (x,(a * y)) = a * (BL . (x,y))

A29: for x being Point of X

for y being Point of Y holds ||.(BL . (x,y)).|| <= (||.f.|| * ||.x.||) * ||.y.||

reconsider BLp = BL as Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Def9;

I . f = BL by FUNCT_1:49;

hence I . f is Lipschitzian BilinearOperator of X,Y,Z ; :: thesis: ( I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| ) )

BLp in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ;

hence I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by FUNCT_1:49; :: thesis: ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| )

A33: ||.BLp.|| = upper_bound (PreNorms (modetrans (BL,X,Y,Z))) by Def13

.= upper_bound (PreNorms BL) ;

A39: ||.f.|| = upper_bound (PreNorms (modetrans (F,X,(R_NormSpace_of_BoundedLinearOperators (Y,Z))))) by LOPBAN_1:def 13

.= upper_bound (PreNorms F) by LOPBAN_1:29 ;

take BLp ; :: thesis: ( BLp = I . f & ||.f.|| = ||.BLp.|| )

thus ( BLp = I . f & ||.f.|| = ||.BLp.|| ) by A37, A46, FUNCT_1:49, XXREAL_0:1; :: thesis: verum

end;for q being Point of Y ex G being Lipschitzian LinearOperator of Y,Z st

( G = f . p & (I . f) . (p,q) = G . q ) ) & I . f is Lipschitzian BilinearOperator of X,Y,Z & I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| ) )

A9: I . f = I0 . f by FUNCT_1:49;

A10: f in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by A7, TARSKI:def 3;

A11: f is Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by A7, TARSKI:def 3, FUNCT_2:66;

reconsider g = f as Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by A7, TARSKI:def 3, FUNCT_2:66;

reconsider F = f as Lipschitzian LinearOperator of X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def 9;

thus for x being Point of X

for y being Point of Y ex G being Lipschitzian LinearOperator of Y,Z st

( G = f . x & (I . f) . (x,y) = G . y ) :: thesis: ( I . f is Lipschitzian BilinearOperator of X,Y,Z & I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| ) )

proof

reconsider BL = I0 . f as Function of [:X,Y:],Z by A10, FUNCT_2:5, FUNCT_2:66;
let x be Point of X; :: thesis: for y being Point of Y ex G being Lipschitzian LinearOperator of Y,Z st

( G = f . x & (I . f) . (x,y) = G . y )

let y be Point of Y; :: thesis: ex G being Lipschitzian LinearOperator of Y,Z st

( G = f . x & (I . f) . (x,y) = G . y )

g . x = F . x ;

then reconsider G = g . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

take G ; :: thesis: ( G = f . x & (I . f) . (x,y) = G . y )

thus ( G = f . x & (I . f) . (x,y) = G . y ) by A1, A9; :: thesis: verum

end;( G = f . x & (I . f) . (x,y) = G . y )

let y be Point of Y; :: thesis: ex G being Lipschitzian LinearOperator of Y,Z st

( G = f . x & (I . f) . (x,y) = G . y )

g . x = F . x ;

then reconsider G = g . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

take G ; :: thesis: ( G = f . x & (I . f) . (x,y) = G . y )

thus ( G = f . x & (I . f) . (x,y) = G . y ) by A1, A9; :: thesis: verum

A15: for x1, x2 being Point of X

for y being Point of Y holds BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y))

proof

A19:
for x being Point of X
let x1, x2 be Point of X; :: thesis: for y being Point of Y holds BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y))

let y be Point of Y; :: thesis: BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y))

A16: BL . (x1,y) = (F . x1) . y by A1, A11;

A17: BL . (x2,y) = (F . x2) . y by A1, A11;

A18: BL . ((x1 + x2),y) = (F . (x1 + x2)) . y by A1, A11;

F . (x1 + x2) = (F . x1) + (F . x2) by VECTSP_1:def 20;

hence BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y)) by A16, A17, A18, LOPBAN_1:35; :: thesis: verum

end;let y be Point of Y; :: thesis: BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y))

A16: BL . (x1,y) = (F . x1) . y by A1, A11;

A17: BL . (x2,y) = (F . x2) . y by A1, A11;

A18: BL . ((x1 + x2),y) = (F . (x1 + x2)) . y by A1, A11;

F . (x1 + x2) = (F . x1) + (F . x2) by VECTSP_1:def 20;

hence BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y)) by A16, A17, A18, LOPBAN_1:35; :: thesis: verum

for y being Point of Y

for a being Real holds BL . ((a * x),y) = a * (BL . (x,y))

proof

A22:
for x being Point of X
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds BL . ((a * x),y) = a * (BL . (x,y))

let y be Point of Y; :: thesis: for a being Real holds BL . ((a * x),y) = a * (BL . (x,y))

let a be Real; :: thesis: BL . ((a * x),y) = a * (BL . (x,y))

A20: BL . ((a * x),y) = (F . (a * x)) . y by A1, A11;

A21: BL . (x,y) = (F . x) . y by A1, A11;

F . (a * x) = a * (F . x) by LOPBAN_1:def 5;

hence BL . ((a * x),y) = a * (BL . (x,y)) by A20, A21, LOPBAN_1:36; :: thesis: verum

end;for a being Real holds BL . ((a * x),y) = a * (BL . (x,y))

let y be Point of Y; :: thesis: for a being Real holds BL . ((a * x),y) = a * (BL . (x,y))

let a be Real; :: thesis: BL . ((a * x),y) = a * (BL . (x,y))

A20: BL . ((a * x),y) = (F . (a * x)) . y by A1, A11;

A21: BL . (x,y) = (F . x) . y by A1, A11;

F . (a * x) = a * (F . x) by LOPBAN_1:def 5;

hence BL . ((a * x),y) = a * (BL . (x,y)) by A20, A21, LOPBAN_1:36; :: thesis: verum

for y1, y2 being Point of Y holds BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2))

proof

A26:
for x being Point of X
let x be Point of X; :: thesis: for y1, y2 being Point of Y holds BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2))

let y1, y2 be Point of Y; :: thesis: BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2))

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A23: BL . (x,y1) = Fx . y1 by A1, A11;

A24: BL . (x,y2) = Fx . y2 by A1, A11;

BL . (x,(y1 + y2)) = Fx . (y1 + y2) by A1, A11;

hence BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2)) by A23, A24, VECTSP_1:def 20; :: thesis: verum

end;let y1, y2 be Point of Y; :: thesis: BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2))

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A23: BL . (x,y1) = Fx . y1 by A1, A11;

A24: BL . (x,y2) = Fx . y2 by A1, A11;

BL . (x,(y1 + y2)) = Fx . (y1 + y2) by A1, A11;

hence BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2)) by A23, A24, VECTSP_1:def 20; :: thesis: verum

for y being Point of Y

for a being Real holds BL . (x,(a * y)) = a * (BL . (x,y))

proof

reconsider BL = BL as BilinearOperator of X,Y,Z by A15, A19, A22, A26, LOPBAN_8:12;
let x be Point of X; :: thesis: for y being Point of Y

for a being Real holds BL . (x,(a * y)) = a * (BL . (x,y))

let y be Point of Y; :: thesis: for a being Real holds BL . (x,(a * y)) = a * (BL . (x,y))

let a be Real; :: thesis: BL . (x,(a * y)) = a * (BL . (x,y))

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A27: BL . (x,y) = Fx . y by A1, A11;

BL . (x,(a * y)) = Fx . (a * y) by A1, A11;

hence BL . (x,(a * y)) = a * (BL . (x,y)) by A27, LOPBAN_1:def 5; :: thesis: verum

end;for a being Real holds BL . (x,(a * y)) = a * (BL . (x,y))

let y be Point of Y; :: thesis: for a being Real holds BL . (x,(a * y)) = a * (BL . (x,y))

let a be Real; :: thesis: BL . (x,(a * y)) = a * (BL . (x,y))

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A27: BL . (x,y) = Fx . y by A1, A11;

BL . (x,(a * y)) = Fx . (a * y) by A1, A11;

hence BL . (x,(a * y)) = a * (BL . (x,y)) by A27, LOPBAN_1:def 5; :: thesis: verum

A29: for x being Point of X

for y being Point of Y holds ||.(BL . (x,y)).|| <= (||.f.|| * ||.x.||) * ||.y.||

proof

then reconsider BL = BL as Lipschitzian BilinearOperator of X,Y,Z by Def8;
let x be Point of X; :: thesis: for y being Point of Y holds ||.(BL . (x,y)).|| <= (||.f.|| * ||.x.||) * ||.y.||

let y be Point of Y; :: thesis: ||.(BL . (x,y)).|| <= (||.f.|| * ||.x.||) * ||.y.||

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A30: BL . (x,y) = Fx . y by A1, A11;

A31: ||.(Fx . y).|| <= ||.(F . x).|| * ||.y.|| by LOPBAN_1:32;

||.(F . x).|| * ||.y.|| <= (||.f.|| * ||.x.||) * ||.y.|| by LOPBAN_1:32, XREAL_1:64;

hence ||.(BL . (x,y)).|| <= (||.f.|| * ||.x.||) * ||.y.|| by A30, A31, XXREAL_0:2; :: thesis: verum

end;let y be Point of Y; :: thesis: ||.(BL . (x,y)).|| <= (||.f.|| * ||.x.||) * ||.y.||

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A30: BL . (x,y) = Fx . y by A1, A11;

A31: ||.(Fx . y).|| <= ||.(F . x).|| * ||.y.|| by LOPBAN_1:32;

||.(F . x).|| * ||.y.|| <= (||.f.|| * ||.x.||) * ||.y.|| by LOPBAN_1:32, XREAL_1:64;

hence ||.(BL . (x,y)).|| <= (||.f.|| * ||.x.||) * ||.y.|| by A30, A31, XXREAL_0:2; :: thesis: verum

reconsider BLp = BL as Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Def9;

I . f = BL by FUNCT_1:49;

hence I . f is Lipschitzian BilinearOperator of X,Y,Z ; :: thesis: ( I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| ) )

BLp in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ;

hence I . f in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by FUNCT_1:49; :: thesis: ex Ix being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) st

( Ix = I . f & ||.f.|| = ||.Ix.|| )

A33: ||.BLp.|| = upper_bound (PreNorms (modetrans (BL,X,Y,Z))) by Def13

.= upper_bound (PreNorms BL) ;

now :: thesis: for r being Real st r in PreNorms BL holds

r <= ||.f.||

then A37:
||.BLp.|| <= ||.f.||
by A33, SEQ_4:45;r <= ||.f.||

let r be Real; :: thesis: ( r in PreNorms BL implies r <= ||.f.|| )

assume r in PreNorms BL ; :: thesis: r <= ||.f.||

then consider t being VECTOR of X, s being VECTOR of Y such that

A34: r = ||.(BL . (t,s)).|| and

A35: ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

A36: ||.(BL . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by A29;

||.t.|| * ||.s.|| <= 1 * 1 by A35, XREAL_1:66;

then ||.f.|| * (||.t.|| * ||.s.||) <= ||.f.|| * 1 by XREAL_1:64;

hence r <= ||.f.|| by A34, A36, XXREAL_0:2; :: thesis: verum

end;assume r in PreNorms BL ; :: thesis: r <= ||.f.||

then consider t being VECTOR of X, s being VECTOR of Y such that

A34: r = ||.(BL . (t,s)).|| and

A35: ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

A36: ||.(BL . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by A29;

||.t.|| * ||.s.|| <= 1 * 1 by A35, XREAL_1:66;

then ||.f.|| * (||.t.|| * ||.s.||) <= ||.f.|| * 1 by XREAL_1:64;

hence r <= ||.f.|| by A34, A36, XXREAL_0:2; :: thesis: verum

A39: ||.f.|| = upper_bound (PreNorms (modetrans (F,X,(R_NormSpace_of_BoundedLinearOperators (Y,Z))))) by LOPBAN_1:def 13

.= upper_bound (PreNorms F) by LOPBAN_1:29 ;

now :: thesis: for r being Real st r in PreNorms F holds

r <= ||.BLp.||

then A46:
||.f.|| <= ||.BLp.||
by A39, SEQ_4:45;r <= ||.BLp.||

let r be Real; :: thesis: ( r in PreNorms F implies r <= ||.BLp.|| )

assume r in PreNorms F ; :: thesis: r <= ||.BLp.||

then consider x being VECTOR of X such that

A40: r = ||.(F . x).|| and

A41: ||.x.|| <= 1 ;

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A42: ||.(F . x).|| = upper_bound (PreNorms Fx) by LOPBAN_1:30;

end;assume r in PreNorms F ; :: thesis: r <= ||.BLp.||

then consider x being VECTOR of X such that

A40: r = ||.(F . x).|| and

A41: ||.x.|| <= 1 ;

reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A42: ||.(F . x).|| = upper_bound (PreNorms Fx) by LOPBAN_1:30;

now :: thesis: for s being Real st s in PreNorms Fx holds

s <= ||.BLp.||

hence
r <= ||.BLp.||
by A40, A42, SEQ_4:45; :: thesis: verums <= ||.BLp.||

let s be Real; :: thesis: ( s in PreNorms Fx implies s <= ||.BLp.|| )

assume s in PreNorms Fx ; :: thesis: s <= ||.BLp.||

then consider y being Point of Y such that

B42: s = ||.(Fx . y).|| and

A43: ||.y.|| <= 1 ;

A44: ||.(Fx . y).|| = ||.(BL . (x,y)).|| by A1, A11;

A45: ||.(BL . (x,y)).|| <= (||.BLp.|| * ||.x.||) * ||.y.|| by Th32;

||.x.|| * ||.y.|| <= 1 * 1 by A41, A43, XREAL_1:66;

then ||.BLp.|| * (||.x.|| * ||.y.||) <= ||.BLp.|| * 1 by XREAL_1:64;

hence s <= ||.BLp.|| by B42, A44, A45, XXREAL_0:2; :: thesis: verum

end;assume s in PreNorms Fx ; :: thesis: s <= ||.BLp.||

then consider y being Point of Y such that

B42: s = ||.(Fx . y).|| and

A43: ||.y.|| <= 1 ;

A44: ||.(Fx . y).|| = ||.(BL . (x,y)).|| by A1, A11;

A45: ||.(BL . (x,y)).|| <= (||.BLp.|| * ||.x.||) * ||.y.|| by Th32;

||.x.|| * ||.y.|| <= 1 * 1 by A41, A43, XREAL_1:66;

then ||.BLp.|| * (||.x.|| * ||.y.||) <= ||.BLp.|| * 1 by XREAL_1:64;

hence s <= ||.BLp.|| by B42, A44, A45, XXREAL_0:2; :: thesis: verum

take BLp ; :: thesis: ( BLp = I . f & ||.f.|| = ||.BLp.|| )

thus ( BLp = I . f & ||.f.|| = ||.BLp.|| ) by A37, A46, FUNCT_1:49, XXREAL_0:1; :: thesis: verum

then reconsider I = I as Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))), the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by FUNCT_2:6;

A47: for x1, x2 being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds I . (x1 + x2) = (I . x1) + (I . x2)

proof

for x being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z))))
let x1, x2 be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))); :: thesis: I . (x1 + x2) = (I . x1) + (I . x2)

for p being Point of X

for q being Point of Y holds (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q))

end;for p being Point of X

for q being Point of Y holds (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q))

proof

hence
I . (x1 + x2) = (I . x1) + (I . x2)
by Th35; :: thesis: verum
let p be Point of X; :: thesis: for q being Point of Y holds (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q))

let q be Point of Y; :: thesis: (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q))

consider Gx1p being Lipschitzian LinearOperator of Y,Z such that

A48: ( Gx1p = x1 . p & (I . x1) . (p,q) = Gx1p . q ) by A8;

consider Gx2p being Lipschitzian LinearOperator of Y,Z such that

A49: ( Gx2p = x2 . p & (I . x2) . (p,q) = Gx2p . q ) by A8;

consider Gx1x2p being Lipschitzian LinearOperator of Y,Z such that

A50: ( Gx1x2p = (x1 + x2) . p & (I . (x1 + x2)) . (p,q) = Gx1x2p . q ) by A8;

(x1 + x2) . p = (x1 . p) + (x2 . p) by LOPBAN_1:35;

hence (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q)) by A48, A49, A50, LOPBAN_1:35; :: thesis: verum

end;let q be Point of Y; :: thesis: (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q))

consider Gx1p being Lipschitzian LinearOperator of Y,Z such that

A48: ( Gx1p = x1 . p & (I . x1) . (p,q) = Gx1p . q ) by A8;

consider Gx2p being Lipschitzian LinearOperator of Y,Z such that

A49: ( Gx2p = x2 . p & (I . x2) . (p,q) = Gx2p . q ) by A8;

consider Gx1x2p being Lipschitzian LinearOperator of Y,Z such that

A50: ( Gx1x2p = (x1 + x2) . p & (I . (x1 + x2)) . (p,q) = Gx1x2p . q ) by A8;

(x1 + x2) . p = (x1 . p) + (x2 . p) by LOPBAN_1:35;

hence (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q)) by A48, A49, A50, LOPBAN_1:35; :: thesis: verum

for a being Real holds I . (a * x) = a * (I . x)

proof

then reconsider I = I as LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by A47, LOPBAN_1:def 5, VECTSP_1:def 20;
let x be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))); :: thesis: for a being Real holds I . (a * x) = a * (I . x)

let a be Real; :: thesis: I . (a * x) = a * (I . x)

for p being Point of X

for q being Point of Y holds (I . (a * x)) . (p,q) = a * ((I . x) . (p,q))

end;let a be Real; :: thesis: I . (a * x) = a * (I . x)

for p being Point of X

for q being Point of Y holds (I . (a * x)) . (p,q) = a * ((I . x) . (p,q))

proof

hence
I . (a * x) = a * (I . x)
by Th36; :: thesis: verum
let p be Point of X; :: thesis: for q being Point of Y holds (I . (a * x)) . (p,q) = a * ((I . x) . (p,q))

let q be Point of Y; :: thesis: (I . (a * x)) . (p,q) = a * ((I . x) . (p,q))

consider Gxp being Lipschitzian LinearOperator of Y,Z such that

A52: ( Gxp = x . p & (I . x) . (p,q) = Gxp . q ) by A8;

consider Gxap being Lipschitzian LinearOperator of Y,Z such that

A53: ( Gxap = (a * x) . p & (I . (a * x)) . (p,q) = Gxap . q ) by A8;

(a * x) . p = a * (x . p) by LOPBAN_1:36;

hence (I . (a * x)) . (p,q) = a * ((I . x) . (p,q)) by A52, A53, LOPBAN_1:36; :: thesis: verum

end;let q be Point of Y; :: thesis: (I . (a * x)) . (p,q) = a * ((I . x) . (p,q))

consider Gxp being Lipschitzian LinearOperator of Y,Z such that

A52: ( Gxp = x . p & (I . x) . (p,q) = Gxp . q ) by A8;

consider Gxap being Lipschitzian LinearOperator of Y,Z such that

A53: ( Gxap = (a * x) . p & (I . (a * x)) . (p,q) = Gxap . q ) by A8;

(a * x) . p = a * (x . p) by LOPBAN_1:36;

hence (I . (a * x)) . (p,q) = a * ((I . x) . (p,q)) by A52, A53, LOPBAN_1:36; :: thesis: verum

A55: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) )

proof

for y being object st y in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))); :: thesis: ( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) )

consider Iu being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) such that

A56: ( Iu = I . u & ||.u.|| = ||.Iu.|| ) by A8;

thus ||.u.|| = ||.(I . u).|| by A56; :: thesis: for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y

let p be Point of X; :: thesis: for y being Point of Y holds (I . u) . (p,y) = (u . p) . y

let q be Point of Y; :: thesis: (I . u) . (p,q) = (u . p) . q

consider G being Lipschitzian LinearOperator of Y,Z such that

A57: ( G = u . p & (I . u) . (p,q) = G . q ) by A8;

thus (I . u) . (p,q) = (u . p) . q by A57; :: thesis: verum

end;for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) )

consider Iu being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) such that

A56: ( Iu = I . u & ||.u.|| = ||.Iu.|| ) by A8;

thus ||.u.|| = ||.(I . u).|| by A56; :: thesis: for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y

let p be Point of X; :: thesis: for y being Point of Y holds (I . u) . (p,y) = (u . p) . y

let q be Point of Y; :: thesis: (I . u) . (p,q) = (u . p) . q

consider G being Lipschitzian LinearOperator of Y,Z such that

A57: ( G = u . p & (I . u) . (p,q) = G . q ) by A8;

thus (I . u) . (p,q) = (u . p) . q by A57; :: thesis: verum

ex x being object st

( x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . x )

proof

then A85:
rng I = the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
by FUNCT_2:10;
let y be object ; :: thesis: ( y in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ex x being object st

( x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . x ) )

assume A59: y in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ; :: thesis: ex x being object st

( x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . x )

then y in Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z) by TARSKI:def 3;

then y in rng I0 by A1, FUNCT_2:def 3;

then consider f being object such that

A60: ( f in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) & I0 . f = y ) by FUNCT_2:11;

reconsider f = f as Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by A60, FUNCT_2:66;

reconsider BL = y as Lipschitzian BilinearOperator of X,Y,Z by A59, Def9;

reconsider BLp = BL as Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Def9;

A62: dom f = the carrier of X by FUNCT_2:def 1;

for x being object st x in the carrier of X holds

f . x in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

A71: for x1, x2 being Point of X holds f . (x1 + x2) = (f . x1) + (f . x2)

for a being Real holds f . (a * x) = a * (f . x)

for x being Point of X holds ||.(f . x).|| <= ||.BLp.|| * ||.x.||

A83: f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) by LOPBAN_1:def 9;

take f ; :: thesis: ( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . f )

thus ( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . f ) by A60, A83, FUNCT_1:49; :: thesis: verum

end;( x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . x ) )

assume A59: y in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ; :: thesis: ex x being object st

( x in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . x )

then y in Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z) by TARSKI:def 3;

then y in rng I0 by A1, FUNCT_2:def 3;

then consider f being object such that

A60: ( f in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) & I0 . f = y ) by FUNCT_2:11;

reconsider f = f as Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by A60, FUNCT_2:66;

reconsider BL = y as Lipschitzian BilinearOperator of X,Y,Z by A59, Def9;

reconsider BLp = BL as Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Def9;

A62: dom f = the carrier of X by FUNCT_2:def 1;

for x being object st x in the carrier of X holds

f . x in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

proof

then reconsider f = f as Function of the carrier of X, the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) by A62, FUNCT_2:3;
let x be object ; :: thesis: ( x in the carrier of X implies f . x in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) )

assume A63: x in the carrier of X ; :: thesis: f . x in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

then reconsider fx = f . x as Function of the carrier of Y, the carrier of Z by FUNCT_2:5, FUNCT_2:66;

reconsider xp = x as Point of X by A63;

A64: for p, q being Point of Y holds fx . (p + q) = (fx . p) + (fx . q)

for a being Real holds fx . (a * p) = a * (fx . p)

for p being Point of Y holds ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) * ||.p.||

fx in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def 9;

hence f . x in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) ; :: thesis: verum

end;assume A63: x in the carrier of X ; :: thesis: f . x in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

then reconsider fx = f . x as Function of the carrier of Y, the carrier of Z by FUNCT_2:5, FUNCT_2:66;

reconsider xp = x as Point of X by A63;

A64: for p, q being Point of Y holds fx . (p + q) = (fx . p) + (fx . q)

proof

for p being Point of Y
let p, q be Point of Y; :: thesis: fx . (p + q) = (fx . p) + (fx . q)

A65: BL . (xp,p) = fx . p by A60, A1;

A66: BL . (xp,q) = fx . q by A60, A1;

BL . (xp,(p + q)) = fx . (p + q) by A60, A1;

hence fx . (p + q) = (fx . p) + (fx . q) by A65, A66, LOPBAN_8:12; :: thesis: verum

end;A65: BL . (xp,p) = fx . p by A60, A1;

A66: BL . (xp,q) = fx . q by A60, A1;

BL . (xp,(p + q)) = fx . (p + q) by A60, A1;

hence fx . (p + q) = (fx . p) + (fx . q) by A65, A66, LOPBAN_8:12; :: thesis: verum

for a being Real holds fx . (a * p) = a * (fx . p)

proof

then reconsider fx = fx as LinearOperator of Y,Z by A64, LOPBAN_1:def 5, VECTSP_1:def 20;
let p be Point of Y; :: thesis: for a being Real holds fx . (a * p) = a * (fx . p)

let a be Real; :: thesis: fx . (a * p) = a * (fx . p)

A68: BL . (xp,p) = fx . p by A60, A1;

BL . (xp,(a * p)) = fx . (a * p) by A60, A1;

hence fx . (a * p) = a * (fx . p) by A68, LOPBAN_8:12; :: thesis: verum

end;let a be Real; :: thesis: fx . (a * p) = a * (fx . p)

A68: BL . (xp,p) = fx . p by A60, A1;

BL . (xp,(a * p)) = fx . (a * p) by A60, A1;

hence fx . (a * p) = a * (fx . p) by A68, LOPBAN_8:12; :: thesis: verum

for p being Point of Y holds ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) * ||.p.||

proof

then reconsider fx = fx as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 8;
let p be Point of Y; :: thesis: ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) * ||.p.||

BL . (xp,p) = fx . p by A60, A1;

hence ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) * ||.p.|| by Th32; :: thesis: verum

end;BL . (xp,p) = fx . p by A60, A1;

hence ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) * ||.p.|| by Th32; :: thesis: verum

fx in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def 9;

hence f . x in the carrier of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) ; :: thesis: verum

A71: for x1, x2 being Point of X holds f . (x1 + x2) = (f . x1) + (f . x2)

proof

for x being Point of X
let x1, x2 be Point of X; :: thesis: f . (x1 + x2) = (f . x1) + (f . x2)

reconsider fx1x2 = f . (x1 + x2) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

reconsider fx1 = f . x1 as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

reconsider fx2 = f . x2 as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

for y being Point of Y holds fx1x2 . y = (fx1 . y) + (fx2 . y)

end;reconsider fx1x2 = f . (x1 + x2) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

reconsider fx1 = f . x1 as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

reconsider fx2 = f . x2 as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

for y being Point of Y holds fx1x2 . y = (fx1 . y) + (fx2 . y)

proof

hence
f . (x1 + x2) = (f . x1) + (f . x2)
by LOPBAN_1:35; :: thesis: verum
let y be Point of Y; :: thesis: fx1x2 . y = (fx1 . y) + (fx2 . y)

A72: BL . (x1,y) = fx1 . y by A60, A1;

A73: BL . (x2,y) = fx2 . y by A60, A1;

BL . ((x1 + x2),y) = fx1x2 . y by A60, A1;

hence fx1x2 . y = (fx1 . y) + (fx2 . y) by A72, A73, LOPBAN_8:12; :: thesis: verum

end;A72: BL . (x1,y) = fx1 . y by A60, A1;

A73: BL . (x2,y) = fx2 . y by A60, A1;

BL . ((x1 + x2),y) = fx1x2 . y by A60, A1;

hence fx1x2 . y = (fx1 . y) + (fx2 . y) by A72, A73, LOPBAN_8:12; :: thesis: verum

for a being Real holds f . (a * x) = a * (f . x)

proof

then reconsider f = f as LinearOperator of X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)) by A71, LOPBAN_1:def 5, VECTSP_1:def 20;
let x be Point of X; :: thesis: for a being Real holds f . (a * x) = a * (f . x)

let a be Real; :: thesis: f . (a * x) = a * (f . x)

reconsider fx = f . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

reconsider fax = f . (a * x) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

for y being Point of Y holds fax . y = a * (fx . y)

end;let a be Real; :: thesis: f . (a * x) = a * (f . x)

reconsider fx = f . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

reconsider fax = f . (a * x) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

for y being Point of Y holds fax . y = a * (fx . y)

proof

hence
f . (a * x) = a * (f . x)
by LOPBAN_1:36; :: thesis: verum
let y be Point of Y; :: thesis: fax . y = a * (fx . y)

A75: BL . (x,y) = fx . y by A60, A1;

BL . ((a * x),y) = fax . y by A60, A1;

hence fax . y = a * (fx . y) by A75, LOPBAN_8:12; :: thesis: verum

end;A75: BL . (x,y) = fx . y by A60, A1;

BL . ((a * x),y) = fax . y by A60, A1;

hence fax . y = a * (fx . y) by A75, LOPBAN_8:12; :: thesis: verum

for x being Point of X holds ||.(f . x).|| <= ||.BLp.|| * ||.x.||

proof

then reconsider f = f as Lipschitzian LinearOperator of X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def 8;
let x be Point of X; :: thesis: ||.(f . x).|| <= ||.BLp.|| * ||.x.||

reconsider fx = f . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A78: for y being Point of Y holds ||.(fx . y).|| <= (||.BLp.|| * ||.x.||) * ||.y.||

end;reconsider fx = f . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

A78: for y being Point of Y holds ||.(fx . y).|| <= (||.BLp.|| * ||.x.||) * ||.y.||

proof

A79:
||.(f . x).|| = upper_bound (PreNorms fx)
by LOPBAN_1:30;
let y be Point of Y; :: thesis: ||.(fx . y).|| <= (||.BLp.|| * ||.x.||) * ||.y.||

BL . (x,y) = fx . y by A60, A1;

hence ||.(fx . y).|| <= (||.BLp.|| * ||.x.||) * ||.y.|| by Th32; :: thesis: verum

end;BL . (x,y) = fx . y by A60, A1;

hence ||.(fx . y).|| <= (||.BLp.|| * ||.x.||) * ||.y.|| by Th32; :: thesis: verum

now :: thesis: for s being Real st s in PreNorms fx holds

s <= ||.BLp.|| * ||.x.||

hence
||.(f . x).|| <= ||.BLp.|| * ||.x.||
by A79, SEQ_4:45; :: thesis: verums <= ||.BLp.|| * ||.x.||

let s be Real; :: thesis: ( s in PreNorms fx implies s <= ||.BLp.|| * ||.x.|| )

assume s in PreNorms fx ; :: thesis: s <= ||.BLp.|| * ||.x.||

then consider y being Point of Y such that

A80: s = ||.(fx . y).|| and

A81: ||.y.|| <= 1 ;

A82: ||.(fx . y).|| <= (||.BLp.|| * ||.x.||) * ||.y.|| by A78;

(||.BLp.|| * ||.x.||) * ||.y.|| <= (||.BLp.|| * ||.x.||) * 1 by A81, XREAL_1:66;

hence s <= ||.BLp.|| * ||.x.|| by A80, A82, XXREAL_0:2; :: thesis: verum

end;assume s in PreNorms fx ; :: thesis: s <= ||.BLp.|| * ||.x.||

then consider y being Point of Y such that

A80: s = ||.(fx . y).|| and

A81: ||.y.|| <= 1 ;

A82: ||.(fx . y).|| <= (||.BLp.|| * ||.x.||) * ||.y.|| by A78;

(||.BLp.|| * ||.x.||) * ||.y.|| <= (||.BLp.|| * ||.x.||) * 1 by A81, XREAL_1:66;

hence s <= ||.BLp.|| * ||.x.|| by A80, A82, XXREAL_0:2; :: thesis: verum

A83: f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) by LOPBAN_1:def 9;

take f ; :: thesis: ( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . f )

thus ( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) & y = I . f ) by A60, A83, FUNCT_1:49; :: thesis: verum

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds ||.(I . u).|| <= 1 * ||.u.|| by A55;

then reconsider I = I as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))),(R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by LOPBAN_1:def 8;

take I ; :: thesis: ( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) )

( I is one-to-one & I is onto ) by A1, A85, FUNCT_1:52, FUNCT_2:def 3;

hence ( I is bijective & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds

( ||.u.|| = ||.(I . u).|| & ( for x being Point of X

for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) ) ) by A55; :: thesis: verum