let X be RealNormSpace; :: thesis: for Y being Subspace of X
for CY being Subset of X st CY = the carrier of Y holds
Cl CY is linearly-closed

let Y be Subspace of X; :: thesis: for CY being Subset of X st CY = the carrier of Y holds
Cl CY is linearly-closed

let CY be Subset of X; :: thesis: ( CY = the carrier of Y implies Cl CY is linearly-closed )
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
proof
let v, u be Point of X; :: thesis: ( v in Cl CY & u in Cl CY implies v + u in Cl CY )
assume A3: ( v in Cl CY & u in Cl CY ) ; :: thesis: v + u in Cl CY
thus v + u in Cl CY :: thesis: verum
proof
consider seqv being sequence of X such that
A4: ( rng seqv c= CY & seqv is convergent & lim seqv = v ) by ;
consider sequ being sequence of X such that
A5: ( rng sequ c= CY & sequ is convergent & lim sequ = u ) by ;
now :: thesis: for y being object st y in rng (seqv + sequ) holds
y in CY
let y be object ; :: thesis: ( y in rng (seqv + sequ) implies y in CY )
assume y in rng (seqv + sequ) ; :: thesis: y in CY
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 ; :: thesis: verum
end;
then A7: rng (seqv + sequ) c= CY ;
lim (seqv + sequ) = v + u by ;
hence v + u in Cl CY by ; :: thesis: verum
end;
end;
for r being Real
for v being Point of X st v in Cl CY holds
r * v in Cl CY
proof
let r be Real; :: thesis: for v being Point of X st v in Cl CY holds
r * v in Cl CY

let v be Point of X; :: thesis: ( v in Cl CY implies r * v in Cl CY )
assume A8: v in Cl CY ; :: thesis: r * v in Cl CY
thus r * v in Cl CY :: thesis: verum
proof
consider seqv being sequence of X such that
A9: ( rng seqv c= CY & seqv is convergent & lim seqv = v ) by ;
A10: ( r * seqv is convergent & lim (r * seqv) = r * (lim seqv) ) by ;
now :: thesis: for y being object st y in rng (r * seqv) holds
y in CY
let y be object ; :: thesis: ( y in rng (r * seqv) implies y in CY )
assume y in rng (r * seqv) ; :: thesis: y in CY
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 ; :: thesis: verum
end;
then rng (r * seqv) c= CY ;
hence r * v in Cl CY by ; :: thesis: verum
end;
end;
hence Cl CY is linearly-closed by A2; :: thesis: verum