let X, Y be RealNormSpace; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ") ) ) ; :: thesis: 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 ; :: thesis: ( 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 ) )

proof

let y, x be object ; :: thesis: ( y in the carrier of (DualSp Y) & S . y = x iff ( x in the carrier of (DualSp X) & T . x = y ) )

hereby :: thesis: ( x in the carrier of (DualSp X) & T . x = y implies ( y in the carrier of (DualSp Y) & S . y = x ) )

assume P31: ( y in the carrier of (DualSp Y) & S . y = x ) ; :: thesis: ( x in the carrier of (DualSp X) & T . x = y )
hence x in the carrier of (DualSp X) by FUNCT_2:5; :: thesis: T . x = y
reconsider yp = y as Point of (DualSp Y) by P31;
reconsider xp = x as Point of (DualSp X) by P31, FUNCT_2:5;
yp is linear-Functional of Y by DUALSP01:def 10;
then G6: dom yp = the carrier of Y by FUNCT_2:def 1;
thus T . x = xp * (L ") by AS1
.= (yp * L) * (L ") by P2, AS5, P31
.= yp * (L * (L ")) by RELAT_1:36
.= yp * (id (rng L)) by AS1, FUNCT_1:39
.= y by G6, AS2, RELAT_1:51 ; :: thesis: verum

end;

assume P32: ( x in the carrier of (DualSp X) & T . x = y ) ; :: thesis: ( y in the carrier of (DualSp Y) & S . y = x )
hence y in the carrier of (DualSp Y) by FUNCT_2:5; :: thesis: S . y = x
reconsider yp = y as Point of (DualSp Y) by P32, FUNCT_2:5;
reconsider xp = x as Point of (DualSp X) by P32;
G5: dom L = the carrier of X by FUNCT_2:def 1;
xp is linear-Functional of X by DUALSP01:def 10;
then G6: dom xp = the carrier of X by FUNCT_2:def 1;
thus S . y = yp * L by P2, AS5
.= (xp * (L ")) * L by AS1, P32
.= xp * ((L ") * L) by RELAT_1:36
.= xp * (id (dom L)) by AS1, FUNCT_1:39
.= x by G6, G5, RELAT_1:51 ; :: thesis: verum

end;

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; :: thesis: verum