theorem Th15: :: LOPBAN14:14

for X, Y being RealNormSpace
for f being Function of X,Y holds
( f is Lipschitzian LinearOperator of X,Y iff f * ((IsoCPNrSP X) ") is Lipschitzian LinearOperator of (product <*X*>),Y )