let X, Y be 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 ) )
let L be 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 ) )
let T be Lipschitzian LinearOperator of (DualSp X),(DualSp Y); ( L is isomorphism & T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) implies 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 ) ) )
assume AS1:
( L is isomorphism & T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) )
; 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 ) )
then AS2:
( L is one-to-one & L is onto & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) )
;
consider K being Lipschitzian LinearOperator of Y,X such that
AS3:
( K = L " & K is isomorphism )
by AS1, NORMSP_3:37;
AS4:
( T is one-to-one & T is onto & ( for x being Point of (DualSp X) holds ||.x.|| = ||.(T . x).|| ) )
by AS1;
consider S being Lipschitzian LinearOperator of (DualSp Y),(DualSp X) such that
AS5:
( S is isomorphism & ( for y being Point of (DualSp Y) holds S . y = y * (K ") ) )
by NISOM09, AS3;
take
S
; ( S is isomorphism & S = T " & ( for y being Point of (DualSp Y) holds S . y = y * L ) )
P2:
K " = L
by FUNCT_1:43, AS1, AS3;
for y, x being object holds
( y in the carrier of (DualSp Y) & S . y = x iff ( x in the carrier of (DualSp X) & T . x = y ) )
hence
( S is isomorphism & S = T " & ( for y being Point of (DualSp Y) holds S . y = y * L ) )
by AS5, P2, FUNCT_2:28, AS4; verum