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