for X being RealNormSpace st not X is trivial holds
ex L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) st L is isomorphism