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

proof

let x be Element of the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: thesis:
reconsider u = x as Lipschitzian BilinearOperator of X,Y,Z by LOPBAN_9:def 4;
u * ((IsoCPNrSP (X,Y)) ") is Lipschitzian MultilinearOperator of <*X,Y*>,Z by IS02A;
then reconsider v = u * ((IsoCPNrSP (X,Y)) ") as Element of the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) by LOPBAN10:def 11;
take v ; :: thesis:
thus S₁[x,v] ; :: thesis:

end;

consider I being Function of the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)), the carrier of (R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) such that
A2: for x being Element of the carrier of (R_NormSpace_of_BoundedBilinearOperators (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_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & x2 in the carrier of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) & I . x1 = I . x2 holds
x1 = x2

proof

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

end;

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

proof

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

end;

then A9: I is onto by FUNCT_2:10;
A12: for x, y being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds I . (x + y) = (I . x) + (I . y)

proof

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

proof

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:19;
A17: (I . x) . xy = x . (((IsoCPNrSP (X,Y)) ") . xy) by A13, FUNCT_2:15
.= x . (p,q) by A16, NDIFF_7:18 ;
A18: (I . y) . xy = y . (((IsoCPNrSP (X,Y)) ") . xy) by A14, FUNCT_2:15
.= y . (p,q) by A16, NDIFF_7:18 ;
(I . (x + y)) . xy = (x + y) . (((IsoCPNrSP (X,Y)) ") . xy) by A15, FUNCT_2:15
.= (x + y) . (p,q) by A16, NDIFF_7:18 ;
hence (I . (x + y)) . xy = ((I . x) . xy) + ((I . y) . xy) by A17, A18, LOPBAN_9:19; :: thesis:

end;

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

end;

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

proof

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

proof

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:19;
A23: (I . x) . xy = x . (((IsoCPNrSP (X,Y)) ") . xy) by A20, FUNCT_2:15
.= x . (p,q) by A22, NDIFF_7:18 ;
(I . (a * x)) . xy = (a * x) . (((IsoCPNrSP (X,Y)) ") . xy) by A21, FUNCT_2:15
.= (a * x) . (p,q) by A22, NDIFF_7:18 ;
hence (I . (a * x)) . xy = a * ((I . x) . xy) by A23, LOPBAN_9:20; :: thesis:

end;

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

end;

then reconsider I = I as LinearOperator of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)),(R_NormSpace_of_BoundedMultilinearOperators (<*X,Y*>,Z)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;
take I ; :: thesis:
A35: dom <*X,Y*> = Seg (len <*X,Y*>) by FINSEQ_1:def 3
.= Seg 2 by FINSEQ_1:44 ;
for u being Element of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds ||.(I . u).|| = ||.u.||

proof

let u be Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: thesis:
reconsider u1 = u as Lipschitzian BilinearOperator of X,Y,Z by LOPBAN_9:def 4;
reconsider v1 = I . u as Lipschitzian MultilinearOperator of <*X,Y*>,Z by LOPBAN10:def 11;
A26: ||.u.|| = upper_bound (PreNorms (modetrans (u,X,Y,Z))) by LOPBAN_9:def 8
.= upper_bound (PreNorms u1) ;
A27: ||.(I . u).|| = upper_bound (PreNorms (modetrans (v1,<*X,Y*>,Z))) by LOPBAN10:def 15
.= upper_bound (PreNorms v1) ;
for z being object holds
( z in PreNorms u1 iff z in PreNorms v1 )

proof

let z be object ; :: thesis:

hereby :: thesis:

assume z in PreNorms u1 ; :: thesis:
then consider x being VECTOR of X, y being VECTOR of Y such that
A28: ( z = ||.(u1 . (x,y)).|| & ||.x.|| <= 1 & ||.y.|| <= 1 ) ;
reconsider s = <*x,y*> as Point of (product <*X,Y*>) by PRVECT_3:19;
A30: v1 . s = (u * ((IsoCPNrSP (X,Y)) ")) . s by A2
.= u . (((IsoCPNrSP (X,Y)) ") . s) by FUNCT_2:15
.= u1 . (x,y) by NDIFF_7:18 ;
for i being Element of dom <*X,Y*> holds ||.(s . i).|| <= 1

proof

let i be Element of dom <*X,Y*>; :: thesis:
( i = 1 or i = 2 ) by FINSEQ_1:2, TARSKI:def 2, A35;
hence ||.(s . i).|| <= 1 by A28; :: thesis:

end;

hence z in PreNorms v1 by A28, A30; :: thesis:

end;

assume z in PreNorms v1 ; :: thesis:
then consider s being VECTOR of (product <*X,Y*>) such that
A31: ( z = ||.(v1 . s).|| & ( for i being Element of dom <*X,Y*> holds ||.(s . i).|| <= 1 ) ) ;
consider x being Point of X, y being Point of Y such that
A32: s = <*x,y*> by PRVECT_3:19;
A33: v1 . s = (u * ((IsoCPNrSP (X,Y)) ")) . s by A2
.= u . (((IsoCPNrSP (X,Y)) ") . s) by FUNCT_2:15
.= u1 . (x,y) by A32, NDIFF_7:18 ;
reconsider i1 = 1, i2 = 2 as Element of dom <*X,Y*> by A35, FINSEQ_1:2, TARSKI:def 2;
( ||.(s . i1).|| <= 1 & ||.(s . i2).|| <= 1 ) by A31;
then ( ||.x.|| <= 1 & ||.y.|| <= 1 ) by A32;
hence z in PreNorms u1 by A31, A33; :: thesis:

end;

hence ||.(I . u).|| = ||.u.|| by A26, A27, TARSKI:2; :: thesis:

end;

hence ( I is bijective & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds I . u = u * ((IsoCPNrSP (X,Y)) ") ) ) by A2, NDIFF_7:7, A3, A9, FUNCT_2:19; :: thesis: