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 (LinearTopSpaceNorm X) such that
A1: ( B is dense & density (LinearTopSpaceNorm X) = 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 A1, EQCL2;
then A3: not A is empty by NONEMP;
A is countable by A1, A2, CARD_3:def 14, TOPGEN_1:def 13;
then consider f being Function of omega,A such that
A4: rng f = A by A3, CARD_3:96;
reconsider seq = f as Function of NAT, the carrier of X by A3, A4, FUNCT_2:6;
reconsider seq = seq as sequence of X ;
rng seq is dense by A1, A4, EQCL2;
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 (LinearTopSpaceNorm X) by NORMSP_2:def 4;
D is dense by A5, EQCL2;
then A6: density (LinearTopSpaceNorm X) c= card D by TOPGEN_1:def 12;
dom seq = NAT by FUNCT_2:def 1;
then card D c= omega by CARD_3:93, CARD_3:def 14;
then density (LinearTopSpaceNorm X) c= omega by A6;
hence X is separable by TOPGEN_1:def 13; :: thesis: verum