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