let X be RealNormSpace; :: thesis: ( X is Reflexive iff Im (BidualFunc X) = DualSp (DualSp X) )
thus ( X is Reflexive implies Im (BidualFunc X) = DualSp (DualSp X) ) by NORMSP_3:46; :: thesis: ( Im (BidualFunc X) = DualSp (DualSp X) implies X is Reflexive )
assume A1: Im (BidualFunc X) = DualSp (DualSp X) ; :: thesis: X is Reflexive
dom (BidualFunc X) <> {} by FUNCT_2:def 1;
then ( rng (BidualFunc X) <> {} & rng (BidualFunc X) is linearly-closed ) by NORMSP_3:35, RELAT_1:42;
then the carrier of (Lin (rng (BidualFunc X))) = rng (BidualFunc X) by NORMSP_3:31;
then BidualFunc X is onto by A1;
hence X is Reflexive ; :: thesis: verum