let X be RealUnitarySpace; :: thesis: for M being Subspace of X
for N being non empty Subset of X st N = the carrier of () holds
( N is linearly-closed & N is closed )

let M be Subspace of X; :: thesis: for N being non empty Subset of X st N = the carrier of () holds
( N is linearly-closed & N is closed )

let N be non empty Subset of X; :: thesis: ( N = the carrier of () implies ( N is linearly-closed & N is closed ) )
assume AS1: N = the carrier of () ; :: thesis: ( N is linearly-closed & N is closed )
hence N is linearly-closed by RUSUB_1:28; :: thesis: N is closed
for s being sequence of X st rng s c= N & s is convergent holds
lim s in N
proof
let s be sequence of X; :: thesis: ( rng s c= N & s is convergent implies lim s in N )
assume AS2: ( rng s c= N & s is convergent ) ; :: thesis: lim s in N
A1: now :: thesis: for i being Nat
for w being VECTOR of X st w in M holds
w .|. (s . i) = 0
let i be Nat; :: thesis: for w being VECTOR of X st w in M holds
w .|. (s . i) = 0

s . i in rng s by ;
then s . i in N by AS2;
then s . i in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal
}
by ;
then consider v being VECTOR of X such that
B1: ( v = s . i & ( for w being VECTOR of X st w in M holds
w,v are_orthogonal ) ) ;
thus for w being VECTOR of X st w in M holds
w .|. (s . i) = 0 by ; :: thesis: verum
end;
for w being VECTOR of X st w in M holds
w .|. (lim s) = 0
proof
let w be VECTOR of X; :: thesis: ( w in M implies w .|. (lim s) = 0 )
assume AS3: w in M ; :: thesis: w .|. (lim s) = 0
reconsider g = w .|. (lim s) as Real ;
for p being Real st 0 < p holds
ex m being Nat st
for n being Nat st m <= n holds
|.((() . n) - (w .|. (lim s))).| < p
proof
let p be Real; :: thesis: ( 0 < p implies ex m being Nat st
for n being Nat st m <= n holds
|.((() . n) - (w .|. (lim s))).| < p )

assume B0: 0 < p ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.((() . n) - (w .|. (lim s))).| < p

B1: 0 <= by BHSP_1:28;
reconsider r = p / ( + 1) as Real ;
B41: ||.w.|| + 0 < + 1 by XREAL_1:8;
r * ( + 1) = p by ;
then B5: ( 0 < r & r * < p ) by ;
consider m being Nat such that
B6: for n being Nat st m <= n holds
||.((s . n) - (lim s)).|| < r by ;
B7: for n being Nat st m <= n holds
|.((() . n) - (w .|. (lim s))).| < p
proof
let n be Nat; :: thesis: ( m <= n implies |.((() . n) - (w .|. (lim s))).| < p )
assume m <= n ; :: thesis: |.((() . n) - (w .|. (lim s))).| < p
then C1: ||.((s . n) - (lim s)).|| < r by B6;
C2: |.((w .|. (s . n)) - (w .|. (lim s))).| = |.(w .|. ((s . n) - (lim s))).| by BHSP_1:12;
C3: |.(w .|. ((s . n) - (lim s))).| <= * ||.((s . n) - (lim s)).|| by BHSP_1:29;
||.w.|| * ||.((s . n) - (lim s)).|| <= * r by ;
then C41: |.((w .|. (s . n)) - (w .|. (lim s))).| <= * r by ;
w .|. (s . n) = 0 by
.= () . n by SEQ_1:57 ;
hence |.((() . n) - (w .|. (lim s))).| < p by ; :: thesis: verum
end;
take m ; :: thesis: for n being Nat st m <= n holds
|.((() . n) - (w .|. (lim s))).| < p

thus for n being Nat st m <= n holds
|.((() . n) - (w .|. (lim s))).| < p by B7; :: thesis: verum
end;
then lim () = w .|. (lim s) by SEQ_2:def 7;
then (seq_const 0) . 0 = w .|. (lim s) by SEQ_4:26;
hence w .|. (lim s) = 0 ; :: thesis: verum
end;
then A3: for w being VECTOR of X st w in M holds
w, lim s are_orthogonal ;
reconsider v = lim s as VECTOR of X ;
lim s in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal
}
by A3;
hence lim s in N by ; :: thesis: verum
end;
hence N is closed by LM1; :: thesis: verum