let X be RealNormSpace; :: thesis:
let Y be Subspace of X; :: thesis:
let CY be Subset of X; :: thesis:
assume A1: CY = the carrier of Y ; :: thesis:
A2: for v, u being Point of X st v in Cl CY & u in Cl CY holds
v + u in Cl CY

let v, u be Point of X; :: thesis:
assume A3: ( v in Cl CY & u in Cl CY ) ; :: thesis:
thus v + u in Cl CY :: thesis:

consider seqv being sequence of X such that
A4: ( rng seqv c= CY & seqv is convergent & lim seqv = v ) by A3, EQCL3;
consider sequ being sequence of X such that
A5: ( rng sequ c= CY & sequ is convergent & lim sequ = u ) by A3, EQCL3;

let y be object ; :: thesis:
assume y in rng (seqv + sequ) ; :: thesis:
then consider x being object such that
A6: ( x in NAT & (seqv + sequ) . x = y ) by FUNCT_2:11;
reconsider x = x as Element of NAT by A6;
( seqv . x in rng seqv & sequ . x in rng sequ ) by FUNCT_2:4;
then ( seqv . x in Y & sequ . x in Y ) by A1, A4, A5;
then (seqv . x) + (sequ . x) in Y by RLSUB_1:20;
hence y in CY by A1, A6, NORMSP_1:def 2; :: thesis:

end;

then A7: rng (seqv + sequ) c= CY ;
lim (seqv + sequ) = v + u by A4, A5, NORMSP_1:25;
hence v + u in Cl CY by A4, A5, A7, EQCL3, NORMSP_1:19; :: thesis:

end;

for r being Real
for v being Point of X st v in Cl CY holds
r * v in Cl CY

consider seqv being sequence of X such that
A9: ( rng seqv c= CY & seqv is convergent & lim seqv = v ) by A8, EQCL3;
A10: ( r * seqv is convergent & lim (r * seqv) = r * (lim seqv) ) by A9, NORMSP_1:22, NORMSP_1:28;

let y be object ; :: thesis:
assume y in rng (r * seqv) ; :: thesis:
then consider x being object such that
A11: ( x in NAT & (r * seqv) . x = y ) by FUNCT_2:11;
reconsider x = x as Element of NAT by A11;
seqv . x in rng seqv by FUNCT_2:4;
then seqv . x in Y by A1, A9;
then r * (seqv . x) in Y by RLSUB_1:21;
hence y in CY by A1, A11, NORMSP_1:def 5; :: thesis:

end;

then rng (r * seqv) c= CY ;
hence r * v in Cl CY by A9, A10, EQCL3; :: thesis:

end;