let X be RealUnitarySpace; :: thesis: for M being Subspace of X
for N being non empty Subset of X st N = the carrier of M holds
Ort_CompSet N = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }
let M be Subspace of X; :: thesis: for N being non empty Subset of X st N = the carrier of M holds
Ort_CompSet N = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }
let N be non empty Subset of X; :: thesis: ( N = the carrier of M implies Ort_CompSet N = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } )
assume A1: N = the carrier of M ; :: thesis: Ort_CompSet N = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }
for z being object holds
( z in Ort_CompSet N iff z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } )

proof

let z be object ; :: thesis: ( z in Ort_CompSet N iff z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } )

hereby :: thesis: ( z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } implies z in Ort_CompSet N )

assume A2: z in Ort_CompSet N ; :: thesis: z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal }
then reconsider x = z as Point of X ;
for w being VECTOR of X st w in M holds
w,x are_orthogonal

proof

let w be VECTOR of X; :: thesis: ( w in M implies w,x are_orthogonal )
assume w in M ; :: thesis: w,x are_orthogonal
then w in N by A1, STRUCT_0:def 5;
hence w,x are_orthogonal by Def1, A2; :: thesis: verum

end;

hence z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } ; :: thesis: verum

end;

assume z in { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } ; :: thesis: z in Ort_CompSet N
then consider v being VECTOR of X such that
A3: ( z = v & ( for w being VECTOR of X st w in M holds
w,v are_orthogonal ) ) ;
for w being VECTOR of X st w in N holds
w .|. v = 0

proof

let w be VECTOR of X; :: thesis: ( w in N implies w .|. v = 0 )
assume w in N ; :: thesis: w .|. v = 0
then w,v are_orthogonal by A3, A1, STRUCT_0:def 5;
hence w .|. v = 0 ; :: thesis: verum

end;

hence z in Ort_CompSet N by A3, Def1; :: thesis: verum

end;

hence Ort_CompSet N = { v where v is VECTOR of X : for w being VECTOR of X st w in M holds
w,v are_orthogonal } by TARSKI:2; :: thesis: verum