let X be RealUnitarySpace; :: thesis: for M being Subspace of X
for N being non empty Subset of X st N = the carrier of (Ort_Comp M) 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 (Ort_Comp M) holds
( N is linearly-closed & N is closed )
let N be non empty Subset of X; :: thesis: ( N = the carrier of (Ort_Comp M) implies ( N is linearly-closed & N is closed ) )
assume AS1: N = the carrier of (Ort_Comp M) ; :: 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 FUNCT_2:4, ORDINAL1:def 12;
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 AS1, RUSUB_5:def 3;
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 B1, BHSP_1:def 3; :: 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
|.(((seq_const 0) . 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
|.(((seq_const 0) . n) - (w .|. (lim s))).| < p )
assume B0: 0 < p ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((seq_const 0) . n) - (w .|. (lim s))).| < p
B1: 0 <= ||.w.|| by BHSP_1:28;
reconsider r = p / (||.w.|| + 1) as Real ;
B41: ||.w.|| + 0 < ||.w.|| + 1 by XREAL_1:8;
r * (||.w.|| + 1) = p by B1, XCMPLX_1:87;
then B5: ( 0 < r & r * ||.w.|| < p ) by B0, B1, B41, XREAL_1:68;
consider m being Nat such that
B6: for n being Nat st m <= n holds
||.((s . n) - (lim s)).|| < r by B1, B0, AS2, BHSP_2:19;
B7: for n being Nat st m <= n holds
|.(((seq_const 0) . n) - (w .|. (lim s))).| < p

proof

let n be Nat; :: thesis: ( m <= n implies |.(((seq_const 0) . n) - (w .|. (lim s))).| < p )
assume m <= n ; :: thesis: |.(((seq_const 0) . 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))).| <= ||.w.|| * ||.((s . n) - (lim s)).|| by BHSP_1:29;
||.w.|| * ||.((s . n) - (lim s)).|| <= ||.w.|| * r by B1, C1, XREAL_1:64;
then C41: |.((w .|. (s . n)) - (w .|. (lim s))).| <= ||.w.|| * r by C2, C3, XXREAL_0:2;
w .|. (s . n) = 0 by A1, AS3
.= (seq_const 0) . n by SEQ_1:57 ;
hence |.(((seq_const 0) . n) - (w .|. (lim s))).| < p by C41, B5, XXREAL_0:2; :: thesis: verum

end;

take m ; :: thesis: for n being Nat st m <= n holds
|.(((seq_const 0) . n) - (w .|. (lim s))).| < p
thus for n being Nat st m <= n holds
|.(((seq_const 0) . n) - (w .|. (lim s))).| < p by B7; :: thesis: verum

end;

then lim (seq_const 0) = 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 AS1, RUSUB_5:def 3; :: thesis: verum

end;

hence N is closed by LM1; :: thesis: verum