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;

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

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 )

given seq being sequence of X such that A5:
rng seq is dense
; :: thesis: 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;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

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