let X, Y, Z be RealLinearSpace; :: thesis:
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_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z))));
set BXYZ = the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z));
set LYZ = the carrier of (R_VectorSpace_of_LinearOperators (Y,Z));

let x be object ; :: thesis:
assume x in Funcs ( the carrier of X, the carrier of (R_VectorSpace_of_LinearOperators (Y,Z))) ; :: thesis:
then consider f being Function such that
A5: ( x = f & dom f = the carrier of X & rng f c= the carrier of (R_VectorSpace_of_LinearOperators (Y,Z)) ) by FUNCT_2:def 2;
rng f c= Funcs ( the carrier of Y, the carrier of Z) by A5, XBOOLE_1:1;
hence x in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by A5, FUNCT_2:def 2; :: thesis:

end;

then A6: Funcs ( the carrier of X, the carrier of (R_VectorSpace_of_LinearOperators (Y,Z))) c= Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by TARSKI:def 3;
then the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))) c= Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by XBOOLE_1:1;
then reconsider I = I0 | the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))) as Function of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z)) by FUNCT_2:32;
A7: for x being Element of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))) holds
( ( for p being Point of X
for q being Point of Y ex G being LinearOperator of Y,Z st
( G = x . p & (I . x) . (p,q) = G . q ) ) & I . x in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) )

proof

let f be Element of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))); :: thesis:
A8: I . f = I0 . f by FUNCT_1:49;
A9: f in Funcs ( the carrier of X,(Funcs ( the carrier of Y, the carrier of Z))) by A6, TARSKI:def 3, XBOOLE_1:1;
then A10: f is Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by FUNCT_2:66;
reconsider g = f as Function of the carrier of X,(Funcs ( the carrier of Y, the carrier of Z)) by A9, FUNCT_2:66;
reconsider F = f as LinearOperator of X,(R_VectorSpace_of_LinearOperators (Y,Z)) by LOPBAN_1:def 6;
thus for x being Point of X
for y being Point of Y ex G being LinearOperator of Y,Z st
( G = f . x & (I . f) . (x,y) = G . y ) :: thesis:

proof

let x be Point of X; :: thesis:
let y be Point of Y; :: thesis:
g . x = F . x ;
then reconsider G = g . x as LinearOperator of Y,Z by LOPBAN_1:def 6;
take G ; :: thesis:
thus ( G = f . x & (I . f) . (x,y) = G . y ) by A1, A8; :: thesis:

end;

reconsider BL = I0 . f as Function of [:X,Y:],Z by A9, FUNCT_2:5, FUNCT_2:66;
A14: 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:
let y be Point of Y; :: thesis:
A15: BL . (x1,y) = (F . x1) . y by A1, A10;
A16: BL . (x2,y) = (F . x2) . y by A1, A10;
A17: BL . ((x1 + x2),y) = (F . (x1 + x2)) . y by A1, A10;
F . (x1 + x2) = (F . x1) + (F . x2) by VECTSP_1:def 20;
hence BL . ((x1 + x2),y) = (BL . (x1,y)) + (BL . (x2,y)) by A15, A16, A17, LOPBAN_1:16; :: thesis:

end;

A18: 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:
let y be Point of Y; :: thesis:
let a be Real; :: thesis:
A19: BL . ((a * x),y) = (F . (a * x)) . y by A1, A10;
A20: BL . (x,y) = (F . x) . y by A1, A10;
F . (a * x) = a * (F . x) by LOPBAN_1:def 5;
hence BL . ((a * x),y) = a * (BL . (x,y)) by A19, A20, LOPBAN_1:17; :: thesis:

end;

A21: 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:
let y1, y2 be Point of Y; :: thesis:
reconsider Fx = F . x as LinearOperator of Y,Z by LOPBAN_1:def 6;
A22: BL . (x,y1) = Fx . y1 by A1, A10;
A23: BL . (x,y2) = Fx . y2 by A1, A10;
BL . (x,(y1 + y2)) = Fx . (y1 + y2) by A1, A10;
hence BL . (x,(y1 + y2)) = (BL . (x,y1)) + (BL . (x,y2)) by A22, A23, VECTSP_1:def 20; :: thesis:

end;

A25: 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:
let y be Point of Y; :: thesis:
let a be Real; :: thesis:
reconsider Fx = F . x as LinearOperator of Y,Z by LOPBAN_1:def 6;
A26: BL . (x,y) = Fx . y by A1, A10;
BL . (x,(a * y)) = Fx . (a * y) by A1, A10;
hence BL . (x,(a * y)) = a * (BL . (x,y)) by A26, LOPBAN_1:def 5; :: thesis:

end;

reconsider BL = BL as BilinearOperator of X,Y,Z by A14, A18, A21, A25, LOPBAN_8:11;
BL in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by Def6;
hence I . f in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by FUNCT_1:49; :: thesis:

end;

then rng I c= the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by FUNCT_2:114;
then reconsider I = I as Function of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))), the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by FUNCT_2:6;
A28: for x1, x2 being Element of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))) holds I . (x1 + x2) = (I . x1) + (I . x2)

proof

let x1, x2 be Element of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))); :: thesis:
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:
let q be Point of Y; :: thesis:
consider Gx1p being LinearOperator of Y,Z such that
A29: ( Gx1p = x1 . p & (I . x1) . (p,q) = Gx1p . q ) by A7;
consider Gx2p being LinearOperator of Y,Z such that
A30: ( Gx2p = x2 . p & (I . x2) . (p,q) = Gx2p . q ) by A7;
consider Gx1x2p being LinearOperator of Y,Z such that
A31: ( Gx1x2p = (x1 + x2) . p & (I . (x1 + x2)) . (p,q) = Gx1x2p . q ) by A7;
(x1 + x2) . p = (x1 . p) + (x2 . p) by LOPBAN_1:16;
hence (I . (x1 + x2)) . (p,q) = ((I . x1) . (p,q)) + ((I . x2) . (p,q)) by A29, A30, A31, LOPBAN_1:16; :: thesis:

end;

hence I . (x1 + x2) = (I . x1) + (I . x2) by Th16; :: thesis:

end;

for x being Element of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z))))
for a being Real holds I . (a * x) = a * (I . x)

proof

let x be Element of the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))); :: thesis:
let a be Real; :: thesis:
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:
let q be Point of Y; :: thesis:
consider Gxp being LinearOperator of Y,Z such that
A33: ( Gxp = x . p & (I . x) . (p,q) = Gxp . q ) by A7;
consider Gxap being LinearOperator of Y,Z such that
A34: ( Gxap = (a * x) . p & (I . (a * x)) . (p,q) = Gxap . q ) by A7;
(a * x) . p = a * (x . p) by LOPBAN_1:17;
hence (I . (a * x)) . (p,q) = a * ((I . x) . (p,q)) by A33, A34, LOPBAN_1:17; :: thesis:

end;

hence I . (a * x) = a * (I . x) by Th17; :: thesis:

end;

then reconsider I = I as LinearOperator of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(R_VectorSpace_of_BilinearOperators (X,Y,Z)) by A28, LOPBAN_1:def 5, VECTSP_1:def 20;
A36: for u being Point of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z))))
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 (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))); :: thesis:
let p be Point of X; :: thesis:
let q be Point of Y; :: thesis:
consider G being LinearOperator of Y,Z such that
A37: ( G = u . p & (I . u) . (p,q) = G . q ) by A7;
thus (I . u) . (p,q) = (u . p) . q by A37; :: thesis:

end;

for y being object st y in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds
ex x being object st
( x in the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))) & y = I . x )

proof

let y be object ; :: thesis:
assume A39: y in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) ; :: thesis:
then y in Funcs ([: the carrier of X, the carrier of Y:], the carrier of Z) ;
then y in rng I0 by A1, FUNCT_2:def 3;
then consider f being object such that
A40: ( 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 A40, FUNCT_2:66;
reconsider BL = y as BilinearOperator of X,Y,Z by A39, Def6;
reconsider BLp = BL as Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by Def6;
A42: 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_VectorSpace_of_LinearOperators (Y,Z))

proof

let x be object ; :: thesis:
assume A43: x in the carrier of X ; :: thesis:
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 A43;
A44: for p, q being Point of Y holds fx . (p + q) = (fx . p) + (fx . q)

proof

let p, q be Point of Y; :: thesis:
A45: BL . (xp,p) = fx . p by A1, A40;
A46: BL . (xp,q) = fx . q by A1, A40;
BL . (xp,(p + q)) = fx . (p + q) by A1, A40;
hence fx . (p + q) = (fx . p) + (fx . q) by A45, A46, LOPBAN_8:11; :: thesis:

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:
let a be Real; :: thesis:
A48: BL . (xp,p) = fx . p by A1, A40;
BL . (xp,(a * p)) = fx . (a * p) by A1, A40;
hence fx . (a * p) = a * (fx . p) by A48, LOPBAN_8:11; :: thesis:

end;

then reconsider fx = fx as LinearOperator of Y,Z by A44, LOPBAN_1:def 5, VECTSP_1:def 20;
fx in the carrier of (R_VectorSpace_of_LinearOperators (Y,Z)) by LOPBAN_1:def 6;
hence f . x in the carrier of (R_VectorSpace_of_LinearOperators (Y,Z)) ; :: thesis:

end;

then reconsider f = f as Function of the carrier of X, the carrier of (R_VectorSpace_of_LinearOperators (Y,Z)) by A42, FUNCT_2:3;
A50: for x1, x2 being Point of X holds f . (x1 + x2) = (f . x1) + (f . x2)

proof

let x1, x2 be Point of X; :: thesis:
reconsider fx1x2 = f . (x1 + x2) as LinearOperator of Y,Z by LOPBAN_1:def 6;
reconsider fx1 = f . x1 as LinearOperator of Y,Z by LOPBAN_1:def 6;
reconsider fx2 = f . x2 as LinearOperator of Y,Z by LOPBAN_1:def 6;
for y being Point of Y holds fx1x2 . y = (fx1 . y) + (fx2 . y)

proof

let y be Point of Y; :: thesis:
A51: BL . (x1,y) = fx1 . y by A1, A40;
A52: BL . (x2,y) = fx2 . y by A1, A40;
BL . ((x1 + x2),y) = fx1x2 . y by A1, A40;
hence fx1x2 . y = (fx1 . y) + (fx2 . y) by A51, A52, LOPBAN_8:11; :: thesis:

end;

hence f . (x1 + x2) = (f . x1) + (f . x2) by LOPBAN_1:16; :: thesis:

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:
let a be Real; :: thesis:
reconsider fx = f . x as LinearOperator of Y,Z by LOPBAN_1:def 6;
reconsider fax = f . (a * x) as LinearOperator of Y,Z by LOPBAN_1:def 6;
for y being Point of Y holds fax . y = a * (fx . y)

proof

let y be Point of Y; :: thesis:
A54: BL . (x,y) = fx . y by A1, A40;
BL . ((a * x),y) = fax . y by A1, A40;
hence fax . y = a * (fx . y) by A54, LOPBAN_8:11; :: thesis:

end;

hence f . (a * x) = a * (f . x) by LOPBAN_1:17; :: thesis:

end;

then reconsider f = f as LinearOperator of X,(R_VectorSpace_of_LinearOperators (Y,Z)) by A50, LOPBAN_1:def 5, VECTSP_1:def 20;
A56: f in the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))) by LOPBAN_1:def 6;
take f ; :: thesis:
thus ( f in the carrier of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))) & y = I . f ) by A40, A56, FUNCT_1:49; :: thesis:

end;

then A58: rng I = the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by FUNCT_2:10;
reconsider I = I as LinearOperator of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(R_VectorSpace_of_BilinearOperators (X,Y,Z)) ;
take I ; :: thesis:
( I is one-to-one & I is onto ) by A1, A58, FUNCT_1:52, FUNCT_2:def 3;
hence ( I is bijective & ( for u being Point of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z))))
for x being Point of X
for y being Point of Y holds (I . u) . (x,y) = (u . x) . y ) ) by A36; :: thesis: