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

for v being Point of X st v in Cl CY holds

r * v in Cl CY

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

for r being Real
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

end;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;

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;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

then A7:
rng (seqv + sequ) c= CY
;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;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

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

for v being Point of X st v in Cl CY holds

r * v in Cl CY

proof

hence
Cl CY is linearly-closed
by A2; :: thesis: verum
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

end;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;

hence r * v in Cl CY by A9, A10, EQCL3; :: thesis: verum

end;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

then
rng (r * seqv) c= CY
;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;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

hence r * v in Cl CY by A9, A10, EQCL3; :: thesis: verum