let X be strict RealNormSpace; :: thesis: for A being non empty Subset of X st ( for f being Point of (DualSp X) st ( for x being Point of X st x in A holds
(Bound2Lipschitz (f,X)) . x = 0 ) holds
Bound2Lipschitz (f,X) = 0. (DualSp X) ) holds
ClNLin A = X
let A be non empty Subset of X; :: thesis: ( ( for f being Point of (DualSp X) st ( for x being Point of X st x in A holds
(Bound2Lipschitz (f,X)) . x = 0 ) holds
Bound2Lipschitz (f,X) = 0. (DualSp X) ) implies ClNLin A = X )
assume A0: for f being Point of (DualSp X) st ( for x being Point of X st x in A holds
(Bound2Lipschitz (f,X)) . x = 0 ) holds
Bound2Lipschitz (f,X) = 0. (DualSp X) ; :: thesis: ClNLin A = X
set M = ClNLin A;
consider Z being Subset of X such that
Q0: ( Z = the carrier of (Lin A) & ClNLin A = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by NORMSP_3:def 20;
reconsider Y = the carrier of (ClNLin A) as non empty Subset of X by DUALSP01:def 16;
Q23: Y is linearly-closed by NORMSP_3:29;
Y = the carrier of X

proof

assume Y <> the carrier of X ; :: thesis: contradiction
then not the carrier of X c= Y ;
then consider x0 being object such that
Q25: ( x0 in the carrier of X & not x0 in Y ) ;
reconsider x0 = x0 as Point of X by Q25;
consider G being Point of (DualSp X) such that
Q26: for x being Point of X st x in Y holds
(Bound2Lipschitz (G,X)) . x = 0 and
Q27: (Bound2Lipschitz (G,X)) . x0 = 1 by Q0, Q23, Q25, DUALSP02:2;
for x being Point of X st x in A holds
(Bound2Lipschitz (G,X)) . x = 0

proof

let x be Point of X; :: thesis: ( x in A implies (Bound2Lipschitz (G,X)) . x = 0 )
assume x in A ; :: thesis: (Bound2Lipschitz (G,X)) . x = 0
then x in Lin A by RLVECT_3:15;
then x in Y by Q0, NORMSP_3:4, TARSKI:def 3;
hence (Bound2Lipschitz (G,X)) . x = 0 by Q26; :: thesis: verum

end;

then (Bound2Lipschitz (G,X)) . x0 = (0. (DualSp X)) . x0 by A0
.= ( the carrier of X --> 0) . x0 by DUALSP01:25
.= 0 ;
hence contradiction by Q27; :: thesis: verum

end;

hence ClNLin A = X by Q0, NORMSP_3:26; :: thesis: verum