let X, Y be RealNormSpace; :: thesis:
assume ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism ; :: thesis:
then consider L being Lipschitzian LinearOperator of X,Y such that
AS: L is isomorphism ;
AS2: ( L is one-to-one & L is onto & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) by AS;
consider T being Lipschitzian LinearOperator of (DualSp X),(DualSp Y) such that
AS1: ( T is isomorphism & ( for x being Point of (DualSp X) holds T . x = x * (L ") ) ) by NISOM09, AS;
DT: dom T = the carrier of (DualSp X) by FUNCT_2:def 1;
assume X is Reflexive ; :: thesis:
then P1: BidualFunc X is onto ;
for y being object st y in the carrier of (DualSp (DualSp Y)) holds
ex x being object st
( x in the carrier of Y & y = (BidualFunc Y) . x )

proof

let y be object ; :: thesis:
assume y in the carrier of (DualSp (DualSp Y)) ; :: thesis:
then reconsider v = y as Point of (DualSp (DualSp Y)) ;
reconsider v = v as Lipschitzian linear-Functional of (DualSp Y) by DUALSP01:def 10;
v * T is Lipschitzian linear-Functional of (DualSp X) by NISOM08;
then reconsider s = v * T as Point of (DualSp (DualSp X)) by DUALSP01:def 10;
consider t being object such that
P2: ( t in the carrier of X & (BidualFunc X) . t = s ) by P1, FUNCT_2:11;
reconsider t = t as Point of X by P2;
set u = L . t;
take L . t ; :: thesis:
for z being Point of (DualSp Y) holds v . z = z . (L . t)

proof

let z be Point of (DualSp Y); :: thesis:
reconsider z0 = z as Lipschitzian linear-Functional of Y by DUALSP01:def 10;
z0 * L is Lipschitzian linear-Functional of X by NISOM08;
then reconsider q = z0 * L as Point of (DualSp X) by DUALSP01:def 10;
R1: BiDual t = s by P2, Def2;
G4: dom L = the carrier of X by FUNCT_2:def 1;
z is Lipschitzian linear-Functional of Y by DUALSP01:def 10;
then G6: dom z = the carrier of Y by FUNCT_2:def 1;
G7: s . q = v . (T . q) by DT, FUNCT_1:13
.= v . (q * (L ")) by AS1
.= v . (z0 * (L * (L "))) by RELAT_1:36
.= v . (z0 * (id (rng L))) by AS, FUNCT_1:39
.= v . z by G6, AS2, RELAT_1:51 ;
s . q = (z0 * L) . t by R1, Def1
.= z . (L . t) by G4, FUNCT_1:13 ;
hence v . z = z . (L . t) by G7; :: thesis:

end;

then y = BiDual (L . t) by Def1;
hence ( L . t in the carrier of Y & y = (BidualFunc Y) . (L . t) ) by Def2; :: thesis:

end;

then BidualFunc Y is onto by FUNCT_2:10;
hence Y is Reflexive ; :: thesis: