let X be RealNormSpace; :: thesis: ( X is Reflexive iff for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x )

hereby :: thesis: ( ( for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x ) implies X is Reflexive )

assume X is Reflexive ; :: thesis: for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x
then A1: BidualFunc X is onto ;
thus for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x :: thesis: verum

proof

let f be Point of (DualSp (DualSp X)); :: thesis: ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x
consider x being object such that
A2: ( x in dom (BidualFunc X) & f = (BidualFunc X) . x ) by A1, FUNCT_1:def 3;
reconsider x = x as Point of X by A2;
take x ; :: thesis: for g being Point of (DualSp X) holds f . g = g . x
f = BiDual x by A2, Def2;
hence for g being Point of (DualSp X) holds f . g = g . x by Def1; :: thesis: verum

end;

end;

assume B1: for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x ; :: thesis: X is Reflexive
for v being object st v in the carrier of (DualSp (DualSp X)) holds
ex s being object st
( s in the carrier of X & v = (BidualFunc X) . s )

proof

let v be object ; :: thesis: ( v in the carrier of (DualSp (DualSp X)) implies ex s being object st
( s in the carrier of X & v = (BidualFunc X) . s ) )
assume v in the carrier of (DualSp (DualSp X)) ; :: thesis: ex s being object st
( s in the carrier of X & v = (BidualFunc X) . s )
then reconsider f = v as Point of (DualSp (DualSp X)) ;
consider s being Point of X such that
B2: for g being Point of (DualSp X) holds f . g = g . s by B1;
take s ; :: thesis: ( s in the carrier of X & v = (BidualFunc X) . s )
thus s in the carrier of X ; :: thesis: v = (BidualFunc X) . s
f = BiDual s by B2, Def1;
hence v = (BidualFunc X) . s by Def2; :: thesis: verum

end;

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