let X be RealHilbertSpace; :: thesis: for M being Subspace of X

for N being Subset of X

for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

let M be Subspace of X; :: thesis: for N being Subset of X

for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

let N be Subset of X; :: thesis: for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

let x be Point of X; :: thesis: ( N = the carrier of M & N is closed implies ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z ) )

assume AS: ( N = the carrier of M & N is closed ) ; :: thesis: ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

set Y = { ||.(x - y).|| where y is Point of X : y in M } ;

{ ||.(x - y).|| where y is Point of X : y in M } c= REAL

0. X in M by RUSUB_1:11;

then ||.(x - (0. X)).|| in Y ;

then reconsider Y = Y as non empty Subset of REAL ;

set d = lower_bound Y;

A11: for r being Real st r in Y holds

0 <= r

consider x0 being Point of X such that

A2: ( lower_bound Y = ||.(x - x0).|| & x0 in M ) by AS, Lm88, A11, SEQ_4:43;

reconsider y = x0 as Point of X ;

reconsider z = x - x0 as Point of X ;

for w being Point of X st w in M holds

w,x - x0 are_orthogonal by A1, A2, Lm87A;

then B21: x - x0 in { v where v is VECTOR of X : for w being Point of X st w in M holds

w,v are_orthogonal } ;

B3: y + z = (x0 + (- x0)) + x by RLVECT_1:def 3

.= x + (0. X) by RLVECT_1:5

.= x ;

take y ; :: thesis: ex z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

take z ; :: thesis: ( y in M & z in Ort_Comp M & x = y + z )

thus ( y in M & z in Ort_Comp M & x = y + z ) by A2, B21, RUSUB_5:def 3, B3; :: thesis: verum

for N being Subset of X

for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

let M be Subspace of X; :: thesis: for N being Subset of X

for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

let N be Subset of X; :: thesis: for x being Point of X st N = the carrier of M & N is closed holds

ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

let x be Point of X; :: thesis: ( N = the carrier of M & N is closed implies ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z ) )

assume AS: ( N = the carrier of M & N is closed ) ; :: thesis: ex y, z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

set Y = { ||.(x - y).|| where y is Point of X : y in M } ;

{ ||.(x - y).|| where y is Point of X : y in M } c= REAL

proof

then reconsider Y = { ||.(x - y).|| where y is Point of X : y in M } as Subset of REAL ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { ||.(x - y).|| where y is Point of X : y in M } or z in REAL )

assume z in { ||.(x - y).|| where y is Point of X : y in M } ; :: thesis: z in REAL

then consider y being Point of X such that

B1: ( z = ||.(x - y).|| & y in M ) ;

thus z in REAL by B1, XREAL_0:def 1; :: thesis: verum

end;assume z in { ||.(x - y).|| where y is Point of X : y in M } ; :: thesis: z in REAL

then consider y being Point of X such that

B1: ( z = ||.(x - y).|| & y in M ) ;

thus z in REAL by B1, XREAL_0:def 1; :: thesis: verum

0. X in M by RUSUB_1:11;

then ||.(x - (0. X)).|| in Y ;

then reconsider Y = Y as non empty Subset of REAL ;

set d = lower_bound Y;

A11: for r being Real st r in Y holds

0 <= r

proof

then A1:
0 <= lower_bound Y
by SEQ_4:43;
let r be Real; :: thesis: ( r in Y implies 0 <= r )

assume r in Y ; :: thesis: 0 <= r

then consider y being Point of X such that

B2: ( r = ||.(x - y).|| & y in M ) ;

thus 0 <= r by B2, BHSP_1:28; :: thesis: verum

end;assume r in Y ; :: thesis: 0 <= r

then consider y being Point of X such that

B2: ( r = ||.(x - y).|| & y in M ) ;

thus 0 <= r by B2, BHSP_1:28; :: thesis: verum

consider x0 being Point of X such that

A2: ( lower_bound Y = ||.(x - x0).|| & x0 in M ) by AS, Lm88, A11, SEQ_4:43;

reconsider y = x0 as Point of X ;

reconsider z = x - x0 as Point of X ;

for w being Point of X st w in M holds

w,x - x0 are_orthogonal by A1, A2, Lm87A;

then B21: x - x0 in { v where v is VECTOR of X : for w being Point of X st w in M holds

w,v are_orthogonal } ;

B3: y + z = (x0 + (- x0)) + x by RLVECT_1:def 3

.= x + (0. X) by RLVECT_1:5

.= x ;

take y ; :: thesis: ex z being Point of X st

( y in M & z in Ort_Comp M & x = y + z )

take z ; :: thesis: ( y in M & z in Ort_Comp M & x = y + z )

thus ( y in M & z in Ort_Comp M & x = y + z ) by A2, B21, RUSUB_5:def 3, B3; :: thesis: verum