let X be RealHilbertSpace; :: thesis: for K being strict Subspace of X
for M being non empty Subset of X st X is strict & the carrier of K is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & Lin M is Subspace of K holds
Ort_Comp (Ort_Comp M) is Subspace of K
let K be strict Subspace of X; :: thesis: for M being non empty Subset of X st X is strict & the carrier of K is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & Lin M is Subspace of K holds
Ort_Comp (Ort_Comp M) is Subspace of K
let M be non empty Subset of X; :: thesis: ( X is strict & the carrier of K is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) & Lin M is Subspace of K implies Ort_Comp (Ort_Comp M) is Subspace of K )
assume that
A1: X is strict and
A2: the carrier of K is closed Subset of (TopSpaceNorm (RUSp2RNSp X)) and
A3: Lin M is Subspace of K ; :: thesis: Ort_Comp (Ort_Comp M) is Subspace of K
reconsider L = the carrier of (Lin M) as non empty Subset of X by RUSUB_1:def 1;
reconsider N = the carrier of K as non empty Subset of X by RUSUB_1:def 1;
reconsider TL = L as Subset of (TopSpaceNorm (RUSp2RNSp X)) ;
A4: the carrier of (Ort_Comp (Ort_Comp M)) = Cl TL by A1, Lm7;
the carrier of (Lin M) c= the carrier of K by RUSUB_1:def 1, A3;
hence Ort_Comp (Ort_Comp M) is Subspace of K by RUSUB_1:22, A2, TOPS_1:5, A4; :: thesis: verum