theorem Th14: :: LOPBAN14:13
for X, Y being RealNormSpace
for f being Function of X,Y holds
( f is LinearOperator of X,Y iff f * ((IsoCPNrSP X) ") is LinearOperator of (product <*X*>),Y )