let X be RealNormSpace; :: thesis: for x being sequence of X holds RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x))

let x be sequence of X; :: thesis: RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x))

set D = RAT_Sums (rng x);

A1: RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x)) by Th17;

the carrier of (NLin (rng x)) c= the carrier of (ClNLin (rng x)) by Th18;

hence RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x)) by A1, XBOOLE_1:1; :: thesis: verum

let x be sequence of X; :: thesis: RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x))

set D = RAT_Sums (rng x);

A1: RAT_Sums (rng x) is Subset of the carrier of (NLin (rng x)) by Th17;

the carrier of (NLin (rng x)) c= the carrier of (ClNLin (rng x)) by Th18;

hence RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x)) by A1, XBOOLE_1:1; :: thesis: verum