let X be RealNormSpace; :: thesis: ( X is separable iff ex seq being sequence of X st rng seq is dense )
set Y = LinearTopSpaceNorm X;
consider B being Subset of such that
A1: ( B is dense & density = card B ) by TOPGEN_1:def 12;
hereby :: thesis: ( ex seq being sequence of X st rng seq is dense implies X is separable )
assume A2: X is separable ; :: thesis: ex seq being sequence of X st rng seq is dense
reconsider A = B as Subset of X by NORMSP_2:def 4;
A is dense by ;
then A3: not A is empty by NONEMP;
A is countable by ;
then consider f being Function of omega,A such that
A4: rng f = A by ;
reconsider seq = f as Function of NAT, the carrier of X by ;
reconsider seq = seq as sequence of X ;
rng seq is dense by ;
hence ex seq being sequence of X st rng seq is dense ; :: thesis: verum
end;
given seq being sequence of X such that A5: rng seq is dense ; :: thesis: X is separable
reconsider D = rng seq as Subset of by NORMSP_2:def 4;
D is dense by ;
then A6: density c= card D by TOPGEN_1:def 12;
dom seq = NAT by FUNCT_2:def 1;
then card D c= omega by ;
then density c= omega by A6;
hence X is separable by TOPGEN_1:def 13; :: thesis: verum