let X be RealUnitarySpace; :: thesis: for M being Subspace of X
for K being Subset of X
for L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st the carrier of M = L & K = Cl L holds
K is linearly-closed
let M be Subspace of X; :: thesis: for K being Subset of X
for L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st the carrier of M = L & K = Cl L holds
K is linearly-closed
let K be Subset of X; :: thesis: for L being Subset of (TopSpaceNorm (RUSp2RNSp X)) st the carrier of M = L & K = Cl L holds
K is linearly-closed
let L be Subset of (TopSpaceNorm (RUSp2RNSp X)); :: thesis: ( the carrier of M = L & K = Cl L implies K is linearly-closed )
assume A1: ( the carrier of M = L & K = Cl L ) ; :: thesis: K is linearly-closed
reconsider CM = the carrier of M as Subset of X by RUSUB_1:def 1;
A3: L c= Cl L by PRE_TOPC:18;
A4: for v, u being VECTOR of X st v in K & u in K holds
v + u in K

proof

let v, u be VECTOR of X; :: thesis: ( v in K & u in K implies v + u in K )
assume A5p: ( v in K & u in K ) ; :: thesis: v + u in K
then consider S being sequence of X such that
A6: ( ( for n being Nat holds S . n in L ) & S is convergent & lim S = v ) by Th10, A1;
consider T being sequence of X such that
A7: ( ( for n being Nat holds T . n in L ) & T is convergent & lim T = u ) by Th10, A5p, A1;
A8: for n being Nat holds (S + T) . n in Cl L

proof

let n be Nat; :: thesis: (S + T) . n in Cl L
A9: (S + T) . n = (S . n) + (T . n) by NORMSP_1:def 2;
( S . n in M & T . n in M ) by A1, STRUCT_0:def 5, A6, A7;
then (S . n) + (T . n) in L by A1, STRUCT_0:def 5, RUSUB_1:14;
hence (S + T) . n in Cl L by A9, A3; :: thesis: verum

end;

lim (S + T) = v + u by BHSP_2:13, A6, A7;
hence v + u in K by A8, A1, BHSP_2:3, A6, A7, Th11; :: thesis: verum

end;

for a being Real
for v being VECTOR of X st v in K holds
a * v in K

proof

let a be Real; :: thesis: for v being VECTOR of X st v in K holds
a * v in K
let v be VECTOR of X; :: thesis: ( v in K implies a * v in K )
assume v in K ; :: thesis: a * v in K
then consider S being sequence of X such that
A11: ( ( for n being Nat holds S . n in L ) & S is convergent & lim S = v ) by Th10, A1;
A12: for n being Nat holds (a * S) . n in Cl L

proof

let n be Nat; :: thesis: (a * S) . n in Cl L
A13: (a * S) . n = a * (S . n) by NORMSP_1:def 5;
S . n in M by A1, STRUCT_0:def 5, A11;
then a * (S . n) in L by A1, STRUCT_0:def 5, RUSUB_1:15;
hence (a * S) . n in Cl L by A13, A3; :: thesis: verum

end;

lim (a * S) = a * v by BHSP_2:15, A11;
hence a * v in K by A12, A1, BHSP_2:5, A11, Th11; :: thesis: verum

end;

hence K is linearly-closed by A4, RLSUB_1:def 1; :: thesis: verum