let X, Y, Z be RealNormSpace; :: thesis: ex I being LinearOperator of ,() st
( I is bijective & ( for u being Point of holds
( = ||.(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 ;
set BXYZ = the carrier of ();
set LYZ = the carrier of ;
A3: the carrier of c= Funcs ( the carrier of Y, the carrier of Z) by XBOOLE_1:1;
A4: the carrier of c= Funcs ( the carrier of X, the carrier of ) by XBOOLE_1:1;
Funcs ( the carrier of X, the carrier of ) c= Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs ( the carrier of X, the carrier of ) 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 ) ; :: 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 ) by FUNCT_2:def 2;
rng f c= Funcs ( the carrier of Y, the carrier of Z) by ;
hence x in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by ; :: thesis: verum
end;
then A7: the carrier of c= Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by ;
then reconsider I = I0 | the carrier of as Function of the carrier of ,(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 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 () & ex Ix being Point of () st
( Ix = I . x & = ||.Ix.|| ) )
proof
let f be Element of the carrier of ; :: 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 () & ex Ix being Point of () st
( Ix = I . 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 ;
A11: f is Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by ;
reconsider g = f as Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by ;
reconsider F = f as Lipschitzian LinearOperator of X, 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 () & ex Ix being Point of () st
( Ix = I . f & = ||.Ix.|| ) )
proof
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;
reconsider BL = I0 . f as Function of [:X,Y:],Z by ;
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
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 ;
A17: BL . (x2,y) = (F . x2) . y by ;
A18: BL . ((x1 + x2),y) = (F . (x1 + x2)) . y by ;
F . (x1 + x2) = (F . x1) + (F . x2) by VECTSP_1:def 20;
hence BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y)) by ; :: thesis: verum
end;
A19: for x being Point of X
for y being Point of Y
for a being Real holds BL . ((a * x),y) = a * (BL . (x,y))
proof
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 ;
A21: BL . (x,y) = (F . x) . y by ;
F . (a * x) = a * (F . x) by LOPBAN_1:def 5;
hence BL . ((a * x),y) = a * (BL . (x,y)) by ; :: thesis: verum
end;
A22: for x being Point of X
for y1, y2 being Point of Y holds BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2))
proof
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 ;
A24: BL . (x,y2) = Fx . y2 by ;
BL . (x,(y1 + y2)) = Fx . (y1 + y2) by ;
hence BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2)) by ; :: thesis: verum
end;
A26: for x being Point of X
for y being Point of Y
for a being Real holds BL . (x,(a * y)) = a * (BL . (x,y))
proof
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 ;
BL . (x,(a * y)) = Fx . (a * y) by ;
hence BL . (x,(a * y)) = a * (BL . (x,y)) by ; :: thesis: verum
end;
reconsider BL = BL as BilinearOperator of X,Y,Z by ;
A29: for x being Point of X
for y being Point of Y holds ||.(BL . (x,y)).|| <= () *
proof
let x be Point of X; :: thesis: for y being Point of Y holds ||.(BL . (x,y)).|| <= () *
let y be Point of Y; :: thesis: ||.(BL . (x,y)).|| <= () *
reconsider Fx = F . x as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
A30: BL . (x,y) = Fx . y by ;
A31: ||.(Fx . y).|| <= ||.(F . x).|| * by LOPBAN_1:32;
||.(F . x).|| * <= () * by ;
hence ||.(BL . (x,y)).|| <= () * by ; :: thesis: verum
end;
then reconsider BL = BL as Lipschitzian BilinearOperator of X,Y,Z by Def8;
reconsider BLp = BL as Point of () 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 () & ex Ix being Point of () st
( Ix = I . f & = ||.Ix.|| ) )

BLp in the carrier of () ;
hence I . f in the carrier of () by FUNCT_1:49; :: thesis: ex Ix being Point of () st
( Ix = I . 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 <=
let r be Real; :: thesis: ( r in PreNorms BL implies r <= )
assume r in PreNorms BL ; :: thesis: r <=
then consider t being VECTOR of X, s being VECTOR of Y such that
A34: r = ||.(BL . (t,s)).|| and
A35: ( ||.t.|| <= 1 & <= 1 ) ;
A36: ||.(BL . (t,s)).|| <= () * by A29;
||.t.|| * <= 1 * 1 by ;
then ||.f.|| * () <= * 1 by XREAL_1:64;
hence r <= by ; :: thesis: verum
end;
then A37: ||.BLp.|| <= by ;
A39: = upper_bound (PreNorms (modetrans (F,X,))) by LOPBAN_1:def 13
.= upper_bound () by LOPBAN_1:29 ;
now :: thesis: for r being Real st r in PreNorms F holds
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;
now :: thesis: for s being Real st s in PreNorms Fx holds
s <= ||.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 ;
A45: ||.(BL . (x,y)).|| <= (||.BLp.|| * ) * by Th32;
||.x.|| * <= 1 * 1 by ;
then ||.BLp.|| * () <= ||.BLp.|| * 1 by XREAL_1:64;
hence s <= ||.BLp.|| by ; :: thesis: verum
end;
hence r <= ||.BLp.|| by ; :: thesis: verum
end;
then A46: ||.f.|| <= ||.BLp.|| by ;
take BLp ; :: thesis: ( BLp = I . f & = ||.BLp.|| )
thus ( BLp = I . f & = ||.BLp.|| ) by ; :: thesis: verum
end;
then rng I c= the carrier of () by FUNCT_2:114;
then reconsider I = I as Function of the carrier of , the carrier of () by FUNCT_2:6;
A47: for x1, x2 being Element of the carrier of holds I . (x1 + x2) = (I . x1) + (I . x2)
proof
let x1, x2 be Element of the carrier of ; :: 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))
proof
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 ; :: thesis: verum
end;
hence I . (x1 + x2) = (I . x1) + (I . x2) by Th35; :: thesis: verum
end;
for x being Element of the carrier of
for a being Real holds I . (a * x) = a * (I . x)
proof
let x be Element of the carrier of ; :: 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))
proof
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 ; :: thesis: verum
end;
hence I . (a * x) = a * (I . x) by Th36; :: thesis: verum
end;
then reconsider I = I as LinearOperator of ,() by ;
A55: for u being Point of holds
( = ||.(I . u).|| & ( for x being Point of X
for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) )
proof
let u be Point of ; :: thesis: ( = ||.(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 () such that
A56: ( Iu = I . 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 object st y in the carrier of () holds
ex x being object st
( x in the carrier of & y = I . x )
proof
let y be object ; :: thesis: ( y in the carrier of () implies ex x being object st
( x in the carrier of & y = I . x ) )

assume A59: y in the carrier of () ; :: thesis: ex x being object st
( x in the carrier of & 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 ;
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 ;
reconsider BL = y as Lipschitzian BilinearOperator of X,Y,Z by ;
reconsider BLp = BL as Point of () 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
proof
let x be object ; :: thesis: ( x in the carrier of X implies f . x in the carrier of )
assume A63: x in the carrier of X ; :: thesis: f . x in the carrier of
then reconsider fx = f . x as Function of the carrier of Y, the carrier of Z by ;
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
let p, q be Point of Y; :: thesis: fx . (p + q) = (fx . p) + (fx . q)
A65: BL . (xp,p) = fx . p by ;
A66: BL . (xp,q) = fx . q by ;
BL . (xp,(p + q)) = fx . (p + q) by ;
hence fx . (p + q) = (fx . p) + (fx . q) by ; :: thesis: verum
end;
for p being Point of Y
for a being Real holds fx . (a * p) = a * (fx . p)
proof
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 ;
BL . (xp,(a * p)) = fx . (a * p) by ;
hence fx . (a * p) = a * (fx . p) by ; :: thesis: verum
end;
then reconsider fx = fx as LinearOperator of Y,Z by ;
for p being Point of Y holds ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) *
proof
let p be Point of Y; :: thesis: ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) *
BL . (xp,p) = fx . p by ;
hence ||.(fx . p).|| <= (||.BLp.|| * ||.xp.||) * by Th32; :: thesis: verum
end;
then reconsider fx = fx as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 8;
fx in the carrier of by LOPBAN_1:def 9;
hence f . x in the carrier of ; :: thesis: verum
end;
then reconsider f = f as Function of the carrier of X, the carrier of by ;
A71: for x1, x2 being Point of X holds f . (x1 + x2) = (f . x1) + (f . x2)
proof
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)
proof
let y be Point of Y; :: thesis: fx1x2 . y = (fx1 . y) + (fx2 . y)
A72: BL . (x1,y) = fx1 . y by ;
A73: BL . (x2,y) = fx2 . y by ;
BL . ((x1 + x2),y) = fx1x2 . y by ;
hence fx1x2 . y = (fx1 . y) + (fx2 . y) by ; :: thesis: verum
end;
hence f . (x1 + x2) = (f . x1) + (f . x2) by LOPBAN_1:35; :: thesis: verum
end;
for x being Point of X
for a being Real holds f . (a * x) = a * (f . x)
proof
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)
proof
let y be Point of Y; :: thesis: fax . y = a * (fx . y)
A75: BL . (x,y) = fx . y by ;
BL . ((a * x),y) = fax . y by ;
hence fax . y = a * (fx . y) by ; :: thesis: verum
end;
hence f . (a * x) = a * (f . x) by LOPBAN_1:36; :: thesis: verum
end;
then reconsider f = f as LinearOperator of X, by ;
for x being Point of X holds ||.(f . x).|| <= ||.BLp.|| *
proof
let x be Point of X; :: thesis: ||.(f . x).|| <= ||.BLp.|| *
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.|| * ) *
proof
let y be Point of Y; :: thesis: ||.(fx . y).|| <= (||.BLp.|| * ) *
BL . (x,y) = fx . y by ;
hence ||.(fx . y).|| <= (||.BLp.|| * ) * by Th32; :: thesis: verum
end;
A79: ||.(f . x).|| = upper_bound (PreNorms fx) by LOPBAN_1:30;
now :: thesis: for s being Real st s in PreNorms fx holds
s <= ||.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
A80: s = ||.(fx . y).|| and
A81: ||.y.|| <= 1 ;
A82: ||.(fx . y).|| <= (||.BLp.|| * ) * by A78;
(||.BLp.|| * ) * <= (||.BLp.|| * ) * 1 by ;
hence s <= ||.BLp.|| * by ; :: thesis: verum
end;
hence ||.(f . x).|| <= ||.BLp.|| * by ; :: thesis: verum
end;
then reconsider f = f as Lipschitzian LinearOperator of X, by LOPBAN_1:def 8;
A83: f in the carrier of by LOPBAN_1:def 9;
take f ; :: thesis: ( f in the carrier of & y = I . f )
thus ( f in the carrier of & y = I . f ) by ; :: thesis: verum
end;
then A85: rng I = the carrier of () by FUNCT_2:10;
for u being Point of holds ||.(I . u).|| <= 1 * by A55;
then reconsider I = I as Lipschitzian LinearOperator of ,() by LOPBAN_1:def 8;
take I ; :: thesis: ( I is bijective & ( for u being Point of holds
( = ||.(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 ;
hence ( I is bijective & ( for u being Point of holds
( = ||.(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