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: Cl CY is linearly-closed
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 A3, EQCL3;
consider sequ being sequence of X such that
A5: ( rng sequ c= CY & sequ is convergent & lim sequ = u ) by A3, EQCL3;

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 A1, A6, NORMSP_1:def 2; :: thesis: verum

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: 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 A8, EQCL3;
A10: ( r * seqv is convergent & lim (r * seqv) = r * (lim seqv) ) by A9, NORMSP_1:22, NORMSP_1:28;

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 A1, A11, NORMSP_1:def 5; :: thesis: verum

end;

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

end;

end;

hence Cl CY is linearly-closed by A2; :: thesis: verum