let V be RealUnitarySpace; :: thesis: for W being Subspace of V holds 0. V in Ort_Comp W
let W be Subspace of V; :: thesis: 0. V in Ort_Comp W
for w being VECTOR of V st w in W holds
w, 0. V are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in W implies w, 0. V are_orthogonal )
assume w in W ; :: thesis: w, 0. V are_orthogonal
w .|. (0. V) = 0 by BHSP_1:15;
hence w, 0. V are_orthogonal by BHSP_1:def 3; :: thesis: verum

end;

then 0. V in { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal } ;
then 0. V in the carrier of (Ort_Comp W) by Def3;
hence 0. V in Ort_Comp W ; :: thesis: verum