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