let X, Y, Z be RealLinearSpace; :: thesis: ex I being LinearOperator of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) st
( 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 ) )
consider I being LinearOperator of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(R_VectorSpace_of_BilinearOperators (X,Y,Z)) such that
A1: ( 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 LOPBAN_9:26;
consider J being LinearOperator of (R_VectorSpace_of_BilinearOperators (X,Y,Z)),(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) such that
A2: ( J is bijective & ( for u being Point of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds J . u = u * ((IsoCPRLSP (X,Y)) ") ) ) by IS03;
reconsider K = J * I as LinearOperator of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))),(R_VectorSpace_of_MultilinearOperators (<*X,Y*>,Z)) by LOPBAN_2:1;
take K ; :: thesis: ( K 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 (K . u) . <*x,y*> = (u . x) . y ) )
thus K is bijective by A1, A2, FUNCT_2:27; :: thesis: 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 (K . u) . <*x,y*> = (u . x) . y
let u be Point of (R_VectorSpace_of_LinearOperators (X,(R_VectorSpace_of_LinearOperators (Y,Z)))); :: thesis: for x being Point of X
for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y
let x be Point of X; :: thesis: for y being Point of Y holds (K . u) . <*x,y*> = (u . x) . y
let y be Point of Y; :: thesis: (K . u) . <*x,y*> = (u . x) . y
A3: K . u = J . (I . u) by FUNCT_2:15;
reconsider xy = <*x,y*> as Point of (product <*X,Y*>) by PRVECT_3:14;
thus (K . u) . <*x,y*> = ((I . u) * ((IsoCPRLSP (X,Y)) ")) . xy by A2, A3
.= (I . u) . (((IsoCPRLSP (X,Y)) ") . xy) by FUNCT_2:15
.= (I . u) . (x,y) by defISOA1
.= (u . x) . y by A1 ; :: thesis: verum