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

for D being Subset of the carrier of (NLin (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 (NLin (rng x)) st D = RAT_Sums (rng x) holds

D is dense

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

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

for S being Subset of (NLin (rng x)) st S <> {} & S is open holds

D meets S

for D being Subset of the carrier of (NLin (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 (NLin (rng x)) st D = RAT_Sums (rng x) holds

D is dense

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

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

for S being Subset of (NLin (rng x)) st S <> {} & S is open holds

D meets S

proof

hence
D is dense
by NORMSP_3:17; :: thesis: verum
let S be Subset of (NLin (rng x)); :: thesis: ( S <> {} & S is open implies D meets S )

assume A2: ( S <> {} & S is open ) ; :: thesis: D meets S

consider z being object such that

A3: z in S by A2, XBOOLE_0:def 1;

reconsider z = z as Point of (NLin (rng x)) by A3;

consider e being Real such that

A4: ( 0 < e & { y where y is Point of (NLin (rng x)) : ||.(y - z).|| < e } c= S ) by A2, A3, NDIFF_1:3;

z in Lin (rng x) ;

then consider l being Linear_Combination of rng x such that

A5: z = Sum l by RLVECT_3:14;

consider m being Linear_Combination of rng x such that

A6: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) by A4, Th23;

Sum m in Lin (rng x) by RLVECT_3:14;

then reconsider y = Sum m as Point of (NLin (rng x)) ;

- (Sum m) = (- 1) * (Sum m) by RLVECT_1:16

.= (- 1) * y by NORMSP_3:28

.= - y by RLVECT_1:16 ;

then (Sum l) - (Sum m) = z - y by A5, NORMSP_3:28;

then ||.((Sum l) - (Sum m)).|| = ||.(z - y).|| by NORMSP_3:28;

then ||.(y - z).|| < e by A6, NORMSP_1:7;

then A8: y in { v where v is Point of (NLin (rng x)) : ||.(v - z).|| < e } ;

y in D by A1, A6;

hence D meets S by A4, A8, XBOOLE_0:def 4; :: thesis: verum

end;assume A2: ( S <> {} & S is open ) ; :: thesis: D meets S

consider z being object such that

A3: z in S by A2, XBOOLE_0:def 1;

reconsider z = z as Point of (NLin (rng x)) by A3;

consider e being Real such that

A4: ( 0 < e & { y where y is Point of (NLin (rng x)) : ||.(y - z).|| < e } c= S ) by A2, A3, NDIFF_1:3;

z in Lin (rng x) ;

then consider l being Linear_Combination of rng x such that

A5: z = Sum l by RLVECT_3:14;

consider m being Linear_Combination of rng x such that

A6: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) by A4, Th23;

Sum m in Lin (rng x) by RLVECT_3:14;

then reconsider y = Sum m as Point of (NLin (rng x)) ;

- (Sum m) = (- 1) * (Sum m) by RLVECT_1:16

.= (- 1) * y by NORMSP_3:28

.= - y by RLVECT_1:16 ;

then (Sum l) - (Sum m) = z - y by A5, NORMSP_3:28;

then ||.((Sum l) - (Sum m)).|| = ||.(z - y).|| by NORMSP_3:28;

then ||.(y - z).|| < e by A6, NORMSP_1:7;

then A8: y in { v where v is Point of (NLin (rng x)) : ||.(v - z).|| < e } ;

y in D by A1, A6;

hence D meets S by A4, A8, XBOOLE_0:def 4; :: thesis: verum