let X be RealUnitarySpace; :: thesis: for M being Subspace of X
for x being Point of X st x in the carrier of M /\ the carrier of (Ort_Comp M) holds
x = 0. X
let M be Subspace of X; :: thesis: for x being Point of X st x in the carrier of M /\ the carrier of (Ort_Comp M) holds
x = 0. X
let x be Point of X; :: thesis: ( x in the carrier of M /\ the carrier of (Ort_Comp M) implies x = 0. X )
assume x in the carrier of M /\ the carrier of (Ort_Comp M) ; :: thesis: x = 0. X
then A1: ( x in M & x in Ort_Comp M ) by XBOOLE_0:def 4;
then x in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } by RUSUB_5:def 3;
then consider v being VECTOR of X such that
A2: ( x = v & ( for w being VECTOR of X st w in M holds
w,v are_orthogonal ) ) ;
x,x are_orthogonal by A1, A2;
hence x = 0. X by BHSP_1:def 2; :: thesis: verum