for X being RealNormSpace st not X is trivial holds
( BidualFunc X is LinearOperator of X,(DualSp (DualSp X)) & ( for x being Point of X holds ||.x.|| = ||.((BidualFunc X) . x).|| ) ) by LMNORM;