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

proof

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;

then reconsider Y = { ||.(x - y).|| where y is Point of X : y in M } as Subset of 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

proof

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;

then A1: 0 <= lower_bound Y by SEQ_4:43;
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