let X be RealNormSpace; ( 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 ( ex seq being sequence of X st rng seq is dense implies X is separable )
assume A2:
X is
separable
;
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
;
verum
end;
given seq being sequence of X such that A5:
rng seq is dense
; 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; verum