let X be RealNormSpace; :: thesis: for x being sequence of X

for D being Subset of the carrier of (ClNLin (rng x)) st D = RAT_Sums (rng x) holds

D is dense

let x be sequence of X; :: thesis: for D being Subset of the carrier of (ClNLin (rng x)) st D = RAT_Sums (rng x) holds

D is dense

let D be Subset of the carrier of (ClNLin (rng x)); :: thesis: ( D = RAT_Sums (rng x) implies D is dense )

assume A1: D = RAT_Sums (rng x) ; :: thesis: D is dense

then reconsider D0 = D as Subset of the carrier of (NLin (rng x)) by Th17;

A2: D0 is dense by A1, Th24;

ex Z being Subset of X st

( Z = the carrier of (NLin (rng x)) & Cl Z = the carrier of (ClNLin (rng x)) ) by Th18;

hence D is dense by A2, Th3; :: thesis: verum

for D being Subset of the carrier of (ClNLin (rng x)) st D = RAT_Sums (rng x) holds

D is dense

let x be sequence of X; :: thesis: for D being Subset of the carrier of (ClNLin (rng x)) st D = RAT_Sums (rng x) holds

D is dense

let D be Subset of the carrier of (ClNLin (rng x)); :: thesis: ( D = RAT_Sums (rng x) implies D is dense )

assume A1: D = RAT_Sums (rng x) ; :: thesis: D is dense

then reconsider D0 = D as Subset of the carrier of (NLin (rng x)) by Th17;

A2: D0 is dense by A1, Th24;

ex Z being Subset of X st

( Z = the carrier of (NLin (rng x)) & Cl Z = the carrier of (ClNLin (rng x)) ) by Th18;

hence D is dense by A2, Th3; :: thesis: verum