let X be RealNormSpace; :: thesis: ( not X is trivial implies ex L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) st L is isomorphism )
assume not X is trivial ; :: thesis: ex L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) st L is isomorphism
then consider DuX being SubRealNormSpace of DualSp (DualSp X), L being Lipschitzian LinearOperator of X,DuX such that
A1: ( L is bijective & DuX = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) ) by IMDDX;
L is isomorphism by A1;
hence ex L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) st L is isomorphism by A1; :: thesis: verum