let X, Y be RealNormSpace-Sequence; :: thesis: for Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedBilinearOperators ((product X),(product Y),Z)) holds f * ((IsoCPNrSP ((product X),(product Y))) ") is Point of (R_NormSpace_of_BoundedMultilinearOperators (<*(product X),(product Y)*>,Z))
let Z be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedBilinearOperators ((product X),(product Y),Z)) holds f * ((IsoCPNrSP ((product X),(product Y))) ") is Point of (R_NormSpace_of_BoundedMultilinearOperators (<*(product X),(product Y)*>,Z))
let f be Point of (R_NormSpace_of_BoundedBilinearOperators ((product X),(product Y),Z)); :: thesis: f * ((IsoCPNrSP ((product X),(product Y))) ") is Point of (R_NormSpace_of_BoundedMultilinearOperators (<*(product X),(product Y)*>,Z))
f is Lipschitzian BilinearOperator of (product X),(product Y),Z by LOPBAN_9:def 4;
then f * ((IsoCPNrSP ((product X),(product Y))) ") is Lipschitzian MultilinearOperator of <*(product X),(product Y)*>,Z by LOPBAN12:13;
hence f * ((IsoCPNrSP ((product X),(product Y))) ") is Point of (R_NormSpace_of_BoundedMultilinearOperators (<*(product X),(product Y)*>,Z)) by LOPBAN10:def 11; :: thesis: verum