let X, Y be RealNormSpace; :: thesis: for f being Function of (product <*X*>),Y holds
( f is LinearOperator of (product <*X*>),Y iff f * (IsoCPNrSP X) is LinearOperator of X,Y )
let f be Function of (product <*X*>),Y; :: thesis: ( f is LinearOperator of (product <*X*>),Y iff f * (IsoCPNrSP X) is LinearOperator of X,Y )
set g = f * (IsoCPNrSP X);
rng (IsoCPNrSP X) = the carrier of (product <*X*>) by FUNCT_2:def 3;
then A1: (IsoCPNrSP X) * ((IsoCPNrSP X) ") = id the carrier of (product <*X*>) by FUNCT_2:29;
(f * (IsoCPNrSP X)) * ((IsoCPNrSP X) ") = f * ((IsoCPNrSP X) * ((IsoCPNrSP X) ")) by RELAT_1:36
.= f by A1, FUNCT_2:17 ;
hence ( f is LinearOperator of (product <*X*>),Y iff f * (IsoCPNrSP X) is LinearOperator of X,Y ) by Th14; :: thesis: verum