theorem Th16: :: LOPBAN14:15

for X, Y being RealNormSpace
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 )