for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y st L is isomorphism holds
ex T being Lipschitzian LinearOperator of (DualSp X),(DualSp Y) st
( T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) )