theorem Th17: :: LOPBAN14:16
for X, Y being RealNormSpace
for f being Function of (product <*X*>),Y holds
( f is Lipschitzian LinearOperator of (product <*X*>),Y iff f * (IsoCPNrSP X) is Lipschitzian LinearOperator of X,Y )