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