theorem :: DUALSP02:27

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