let X, Y be RealNormSpace; :: thesis: 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 ") ) )
let L be Lipschitzian LinearOperator of X,Y; :: thesis: ( L is isomorphism implies 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 ") ) ) )
assume AS: L is isomorphism ; :: thesis: 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 ") ) )
then AS1: ( 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
AS2: ( K = L " & K is isomorphism ) by AS, NORMSP_3:37;
D1: dom K = the carrier of Y by FUNCT_2:def 1;
defpred S₁[ Function, Function] means $2 = $1 * K;
P0: for x being Element of (DualSp X) ex y being Element of (DualSp Y) st S₁[x,y]

proof

let x be Element of (DualSp X); :: thesis: ex y being Element of (DualSp Y) st S₁[x,y]
x is Lipschitzian linear-Functional of X by DUALSP01:def 10;
then x * K is Lipschitzian linear-Functional of Y by NISOM08;
then reconsider y = x * K as Element of (DualSp Y) by DUALSP01:def 10;
take y ; :: thesis: S₁[x,y]
thus y = x * K ; :: thesis: verum

end;

consider T being Function of (DualSp X),(DualSp Y) such that
P1: for x being Element of (DualSp X) holds S₁[x,T . x] from FUNCT_2:sch 3(P0);
for v, w being Point of (DualSp X) holds T . (v + w) = (T . v) + (T . w)

proof

let v, w be Point of (DualSp X); :: thesis: T . (v + w) = (T . v) + (T . w)
P21: ( T . v = v * K & T . w = w * K & T . (v + w) = (v + w) * K ) by P1;
for t being VECTOR of Y holds (T . (v + w)) . t = ((T . v) . t) + ((T . w) . t)

proof

let t be VECTOR of Y; :: thesis: (T . (v + w)) . t = ((T . v) . t) + ((T . w) . t)
thus (T . (v + w)) . t = (v + w) . (K . t) by P21, D1, FUNCT_1:13
.= (v . (K . t)) + (w . (K . t)) by DUALSP01:29
.= ((T . v) . t) + (w . (K . t)) by P21, D1, FUNCT_1:13
.= ((T . v) . t) + ((T . w) . t) by P21, D1, FUNCT_1:13 ; :: thesis: verum

end;

hence T . (v + w) = (T . v) + (T . w) by DUALSP01:29; :: thesis: verum

end;

then P3: T is additive ;
for v being Point of (DualSp X)
for r being Real holds T . (r * v) = r * (T . v)

proof

let v be Point of (DualSp X); :: thesis: for r being Real holds T . (r * v) = r * (T . v)
let r be Real; :: thesis: T . (r * v) = r * (T . v)
P21: ( T . v = v * K & T . (r * v) = (r * v) * K ) by P1;
for t being VECTOR of Y holds (T . (r * v)) . t = r * ((T . v) . t)

proof

let t be VECTOR of Y; :: thesis: (T . (r * v)) . t = r * ((T . v) . t)
thus (T . (r * v)) . t = (r * v) . (K . t) by P21, D1, FUNCT_1:13
.= r * (v . (K . t)) by DUALSP01:30
.= r * ((T . v) . t) by P21, D1, FUNCT_1:13 ; :: thesis: verum

end;

hence T . (r * v) = r * (T . v) by DUALSP01:30; :: thesis: verum

end;

then reconsider T = T as LinearOperator of (DualSp X),(DualSp Y) by P3, LOPBAN_1:def 5;
for v being object st v in the carrier of (DualSp Y) holds
ex s being object st
( s in the carrier of (DualSp X) & v = T . s )

proof

let v be object ; :: thesis: ( v in the carrier of (DualSp Y) implies ex s being object st
( s in the carrier of (DualSp X) & v = T . s ) )
assume v in the carrier of (DualSp Y) ; :: thesis: ex s being object st
( s in the carrier of (DualSp X) & v = T . s )
then reconsider y = v as Lipschitzian linear-Functional of Y by DUALSP01:def 10;
y * L is Lipschitzian linear-Functional of X by NISOM08;
then reconsider s = y * L as Point of (DualSp X) by DUALSP01:def 10;
take s ; :: thesis: ( s in the carrier of (DualSp X) & v = T . s )
G6: dom y = the carrier of Y by FUNCT_2:def 1;
T . s = s * K by P1
.= y * (L * K) by RELAT_1:36
.= y * (id (rng L)) by AS2, AS, FUNCT_1:39
.= v by G6, AS1, RELAT_1:51 ;
hence ( s in the carrier of (DualSp X) & v = T . s ) ; :: thesis: verum

end;

then XX: T is onto by FUNCT_2:10;
P5: for v being Point of (DualSp X) holds ||.(T . v).|| = ||.v.||

proof

let v be Point of (DualSp X); :: thesis: ||.(T . v).|| = ||.v.||
P21: T . v = v * K by P1;
reconsider y = T . v as Lipschitzian linear-Functional of Y by DUALSP01:def 10;
reconsider x = v as Lipschitzian linear-Functional of X by DUALSP01:def 10;
for z being object holds
( z in PreNorms x iff z in PreNorms y )

proof

let z be object ; :: thesis: ( z in PreNorms x iff z in PreNorms y )

hereby :: thesis: ( z in PreNorms y implies z in PreNorms x )

assume z in PreNorms x ; :: thesis: z in PreNorms y
then consider t being VECTOR of X such that
B2: ( z = |.(x . t).| & ||.t.|| <= 1 ) ;
D1: dom L = the carrier of X by FUNCT_2:def 1;
D2: dom K = the carrier of Y by FUNCT_2:def 1;
set s = L . t;
K . (L . t) = t by AS, AS2, D1, FUNCT_1:34;
then A81: z = |.(y . (L . t)).| by P21, D2, B2, FUNCT_1:13;
||.(L . t).|| = ||.t.|| by AS;
hence z in PreNorms y by A81, B2; :: thesis: verum

end;

assume z in PreNorms y ; :: thesis: z in PreNorms x
then consider s being VECTOR of Y such that
B2: ( z = |.(y . s).| & ||.s.|| <= 1 ) ;
set t = K . s;
dom K = the carrier of Y by FUNCT_2:def 1;
then A81: z = |.(x . (K . s)).| by B2, P21, FUNCT_1:13;
||.s.|| = ||.(K . s).|| by AS2;
hence z in PreNorms x by A81, B2; :: thesis: verum

end;

then A9: PreNorms x = PreNorms y ;
thus ||.v.|| = upper_bound (PreNorms (Bound2Lipschitz (v,X))) by DUALSP01:def 14
.= upper_bound (PreNorms y) by A9, DUALSP01:23
.= upper_bound (PreNorms (Bound2Lipschitz (y,Y))) by DUALSP01:23
.= ||.(T . v).|| by DUALSP01:def 14 ; :: thesis: verum

end;

then for v being Point of (DualSp X) holds ||.(T . v).|| <= 1 * ||.v.|| ;
then reconsider T = T as Lipschitzian LinearOperator of (DualSp X),(DualSp Y) by LOPBAN_1:def 8;
take T ; :: thesis: ( T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) )
for x1, x2 being object st x1 in the carrier of (DualSp X) & x2 in the carrier of (DualSp X) & T . x1 = T . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in the carrier of (DualSp X) & x2 in the carrier of (DualSp X) & T . x1 = T . x2 implies x1 = x2 )
assume A1: ( x1 in the carrier of (DualSp X) & x2 in the carrier of (DualSp X) & T . x1 = T . x2 ) ; :: thesis: x1 = x2
then reconsider v1 = x1, v2 = x2 as Point of (DualSp X) ;
T . (v1 - v2) = T . (v1 + ((- 1) * v2)) by RLVECT_1:16
.= (T . v1) + (T . ((- 1) * v2)) by VECTSP_1:def 20
.= (T . v1) + ((- 1) * (T . v2)) by LOPBAN_1:def 5
.= (T . v1) + (- (T . v2)) by RLVECT_1:16
.= 0. (DualSp Y) by RLVECT_1:5, A1 ;
then ||.(T . (v1 - v2)).|| = 0 ;
then ||.(v1 - v2).|| = 0 by P5;
hence x1 = x2 by NORMSP_1:6; :: thesis: verum

end;

hence ( T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) ) by P5, XX, P1, AS2, FUNCT_2:19; :: thesis: verum