let X, Y, Z be RealLinearSpace; :: thesis:
set F1 = the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z));
set F2 = the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z));
defpred S₁[ Function, Function] means $2 = $1 * ((IsoCPRLSP (X,Y)) ");
A1: for x being Element of the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) ex y being Element of the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) st S₁[x,y]

let x be Element of the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)); :: thesis:
reconsider u = x as BilinearOperator of X,Y,Z by LOPBAN_9:def 1;
u * ((IsoCPRLSP (X,Y)) ") is MultilinearOperator of <*X,Y*>,Z by IS02;
then reconsider v = u * ((IsoCPRLSP (X,Y)) ") as Element of the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) by LOPBAN10:def 4;
take v ; :: thesis:
thus S₁[x,v] ; :: thesis:

end;

consider I being Function of the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)), the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) such that
A2: for x being Element of the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds S₁[x,I . x] from FUNCT_2:sch 3(A1);
A3: for x1, x2 being object st x1 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & x2 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & I . x1 = I . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis:
assume A4: ( x1 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & x2 in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & I . x1 = I . x2 ) ; :: thesis:
then reconsider u1 = x1, u2 = x2 as Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) ;
reconsider v1 = u1, v2 = u2 as BilinearOperator of X,Y,Z by LOPBAN_9:def 1;
I . v1 = v1 * ((IsoCPRLSP (X,Y)) ") by A2;
then v1 * ((IsoCPRLSP (X,Y)) ") = v2 * ((IsoCPRLSP (X,Y)) ") by A2, A4;
then v1 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y))) = (v2 * ((IsoCPRLSP (X,Y)) ")) * (IsoCPRLSP (X,Y)) by RELAT_1:36;
then A6: v1 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y))) = v2 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y))) by RELAT_1:36;
( IsoCPRLSP (X,Y) is one-to-one & rng (IsoCPRLSP (X,Y)) = the carrier of (product <*X,Y*>) ) by FUNCT_2:def 3;
then A7: ((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y)) = id [:X,Y:] by FUNCT_2:29;
then v1 * (((IsoCPRLSP (X,Y)) ") * (IsoCPRLSP (X,Y))) = v1 by FUNCT_2:17;
hence x1 = x2 by A6, A7, FUNCT_2:17; :: thesis:

end;

A9: for y being object st y in the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) holds
ex x being object st
( x in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) & y = I . x )

let y be object ; :: thesis:
assume y in the carrier of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) ; :: thesis:
then reconsider u = y as Point of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) ;
reconsider u1 = u as MultilinearOperator of <*X,Y*>,Z by LOPBAN10:def 4;
reconsider v1 = u1 * (IsoCPRLSP (X,Y)) as BilinearOperator of X,Y,Z by IS01;
reconsider v = v1 as Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by LOPBAN_9:def 1;
take v ; :: thesis:
thus v in the carrier of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) ; :: thesis:
( IsoCPRLSP (X,Y) is one-to-one & rng (IsoCPRLSP (X,Y)) = the carrier of (product <*X,Y*>) ) by FUNCT_2:def 3;
then A10: (IsoCPRLSP (X,Y)) * ((IsoCPRLSP (X,Y)) ") = id (product <*X,Y*>) by FUNCT_2:29;
thus I . v = (u1 * (IsoCPRLSP (X,Y))) * ((IsoCPRLSP (X,Y)) ") by A2
.= u1 * ((IsoCPRLSP (X,Y)) * ((IsoCPRLSP (X,Y)) ")) by RELAT_1:36
.= y by A10, FUNCT_2:17 ; :: thesis:

end;

A12: for x, y being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds I . (x + y) = (I . x) + (I . y)

let x, y be Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)); :: thesis:
A13: I . x = x * ((IsoCPRLSP (X,Y)) ") by A2;
A14: I . y = y * ((IsoCPRLSP (X,Y)) ") by A2;
A15: I . (x + y) = (x + y) * ((IsoCPRLSP (X,Y)) ") by A2;
reconsider f = I . x, g = I . y, h = I . (x + y) as Point of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) ;
for xy being VECTOR of (product <*X,Y*>) holds h . xy = (f . xy) + (g . xy)

let xy be VECTOR of (product <*X,Y*>); :: thesis:
consider p being Point of X, q being Point of Y such that
A16: xy = <*p,q*> by PRVECT_3:14;
A17: f . xy = x . (((IsoCPRLSP (X,Y)) ") . xy) by A13, FUNCT_2:15
.= x . (p,q) by A16, defISOA1 ;
A18: g . xy = y . (((IsoCPRLSP (X,Y)) ") . xy) by A14, FUNCT_2:15
.= y . (p,q) by A16, defISOA1 ;
h . xy = (x + y) . (((IsoCPRLSP (X,Y)) ") . xy) by A15, FUNCT_2:15
.= (x + y) . (p,q) by A16, defISOA1 ;
hence h . xy = (f . xy) + (g . xy) by A17, A18, LOPBAN_9:2; :: thesis:

end;

hence I . (x + y) = (I . x) + (I . y) by LOPBAN10:11; :: thesis:

end;

for x being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z))
for a being Real holds I . (a * x) = a * (I . x)

let x be Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)); :: thesis:
let a be Real; :: thesis:
A20: I . x = x * ((IsoCPRLSP (X,Y)) ") by A2;
A21: I . (a * x) = (a * x) * ((IsoCPRLSP (X,Y)) ") by A2;
reconsider f = I . x, g = I . (a * x) as Point of (R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) ;
for xy being VECTOR of (product <*X,Y*>) holds g . xy = a * (f . xy)

let xy be VECTOR of (product <*X,Y*>); :: thesis:
consider p being Point of X, q being Point of Y such that
A22: xy = <*p,q*> by PRVECT_3:14;
A23: f . xy = x . (((IsoCPRLSP (X,Y)) ") . xy) by A20, FUNCT_2:15
.= x . (p,q) by A22, defISOA1 ;
g . xy = (a * x) . (((IsoCPRLSP (X,Y)) ") . xy) by A21, FUNCT_2:15
.= (a * x) . (p,q) by A22, defISOA1 ;
hence g . xy = a * (f . xy) by A23, LOPBAN_9:3; :: thesis:

end;

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

end;

then reconsider I = I as LinearOperator of (R_VectorSpace_of_BilinearOperators (X,Y,Z)),(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;
take I ; :: thesis:
( I is one-to-one & I is onto ) by A3, A9, FUNCT_2:10, FUNCT_2:19;
hence ( I is bijective & ( for u being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPRLSP (X,Y)) ") ) ) by A2; :: thesis: