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

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

hence
N is closed
by LM1; :: thesis: verum
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

w .|. (lim s) = 0

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

for w being VECTOR of X st w in M holds 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;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

w .|. (lim s) = 0

proof

then A3:
for w being VECTOR of X st w in M holds
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

then (seq_const 0) . 0 = w .|. (lim s) by SEQ_4:26;

hence w .|. (lim s) = 0 ; :: thesis: verum

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

then
lim (seq_const 0) = w .|. (lim s)
by SEQ_2:def 7;
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

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

take
m
; :: thesis: for n being Nat st m <= n holds
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;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

|.(((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

then (seq_const 0) . 0 = w .|. (lim s) by SEQ_4:26;

hence w .|. (lim s) = 0 ; :: thesis: verum

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