let X be RealHilbertSpace; :: thesis: for M being Subspace of X st X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) holds
X is_the_direct_sum_of M, Ort_Comp M
let M be Subspace of X; :: thesis: ( X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) implies X is_the_direct_sum_of M, Ort_Comp M )
assume A1: ( X is strict & the carrier of M is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) ) ; :: thesis: X is_the_direct_sum_of M, Ort_Comp M
AAT6: for z being object holds
( z in the carrier of (M + (Ort_Comp M)) iff z in the carrier of X )

proof

let z be object ; :: thesis: ( z in the carrier of (M + (Ort_Comp M)) iff z in the carrier of X )

hereby :: thesis: ( z in the carrier of X implies z in the carrier of (M + (Ort_Comp M)) )

assume z in the carrier of (M + (Ort_Comp M)) ; :: thesis: z in the carrier of X
then z in { (v + u) where v, u is VECTOR of X : ( v in M & u in Ort_Comp M ) } by RUSUB_2:def 1;
then ex v, u being VECTOR of X st
( z = v + u & v in M & u in Ort_Comp M ) ;
hence z in the carrier of X ; :: thesis: verum

end;

assume z in the carrier of X ; :: thesis: z in the carrier of (M + (Ort_Comp M))
then reconsider x = z as Point of X ;
consider m0 being Point of X such that
A2: m0 in M and
A3: for m being Point of X st m in M holds
||.(x - m0).|| <= ||.(x - m).|| by Th19, A1;
reconsider CM = the carrier of M as non empty Subset of X by RUSUB_1:def 1;
for m being Point of X st m in M holds
(x - m0) .|. m = 0 by Th17, A2, A3;
then for m being Point of X st m in the carrier of M holds
m .|. (x - m0) = 0 by STRUCT_0:def 5;
then x - m0 in Ort_CompSet CM by Def1;
then x - m0 in the carrier of (Ort_Comp CM) by Lm5;
then x - m0 in Ort_Comp CM by STRUCT_0:def 5;
then A4: x - m0 in Ort_Comp M by Lm6;
z = m0 + (x - m0) by RLVECT_4:1;
then z in { (u + v) where u, v is VECTOR of X : ( u in M & v in Ort_Comp M ) } by A2, A4;
hence z in the carrier of (M + (Ort_Comp M)) by RUSUB_2:def 1; :: thesis: verum

end;

for z being object holds
( z in the carrier of (M /\ (Ort_Comp M)) iff z in {(0. X)} )

proof

let z be object ; :: thesis: ( z in the carrier of (M /\ (Ort_Comp M)) iff z in {(0. X)} )

hereby :: thesis: ( z in {(0. X)} implies z in the carrier of (M /\ (Ort_Comp M)) )

assume z in the carrier of (M /\ (Ort_Comp M)) ; :: thesis: z in {(0. X)}
then z in the carrier of M /\ the carrier of (Ort_Comp M) by RUSUB_2:def 2;
then A7: ( z in the carrier of M & z in the carrier of (Ort_Comp M) ) by XBOOLE_0:def 4;
the carrier of M c= the carrier of X by RUSUB_1:def 1;
then reconsider x = z as Point of X by A7;
reconsider N = the carrier of M as non empty Subset of X by RUSUB_1:def 1;
x in the carrier of (Ort_Comp N) by A7, Lm6;
then x in Ort_CompSet N by Lm5;
then x .|. x = 0 by Def1, A7;
then ||.x.|| = 0 ;
then x = 0. X by BHSP_1:26;
hence z in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

assume z in {(0. X)} ; :: thesis: z in the carrier of (M /\ (Ort_Comp M))
then z = 0. X by TARSKI:def 1;
then ( z in the carrier of M & z in the carrier of (Ort_Comp M) ) by RUSUB_1:11, STRUCT_0:def 5;
then z in the carrier of M /\ the carrier of (Ort_Comp M) by XBOOLE_0:def 4;
hence z in the carrier of (M /\ (Ort_Comp M)) by RUSUB_2:def 2; :: thesis: verum

end;

hence X is_the_direct_sum_of M, Ort_Comp M by AAT6, RUSUB_1:26, A1, TARSKI:2, RUSUB_1:def 2; :: thesis: verum