let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for M being non empty Subset of V st M = the carrier of W holds
Ort_Comp M = Ort_Comp W
let W be Subspace of V; :: thesis: for M being non empty Subset of V st M = the carrier of W holds
Ort_Comp M = Ort_Comp W
let M be non empty Subset of V; :: thesis: ( M = the carrier of W implies Ort_Comp M = Ort_Comp W )
assume A1: M = the carrier of W ; :: thesis: Ort_Comp M = Ort_Comp W
for x being set st x in the carrier of (Ort_Comp M) holds
x in the carrier of (Ort_Comp W)

proof

let x be set ; :: thesis: ( x in the carrier of (Ort_Comp M) implies x in the carrier of (Ort_Comp W) )
assume x in the carrier of (Ort_Comp M) ; :: thesis: x in the carrier of (Ort_Comp W)
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in M holds
w,v are_orthogonal } by Def4;
then consider v being VECTOR of V such that
A2: ( x = v & ( for w being VECTOR of V st w in M holds
w,v are_orthogonal ) ) ;
for w being VECTOR of V st w in W holds
w,v are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in W implies w,v are_orthogonal )
assume w in W ; :: thesis: w,v are_orthogonal
then w in M by A1, STRUCT_0:def 5;
hence w,v are_orthogonal by A2; :: thesis: verum

end;

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

end;

then A3: the carrier of (Ort_Comp M) c= the carrier of (Ort_Comp W) by TARSKI:def 3;
for x being set st x in the carrier of (Ort_Comp W) holds
x in the carrier of (Ort_Comp M)

proof

let x be set ; :: thesis: ( x in the carrier of (Ort_Comp W) implies x in the carrier of (Ort_Comp M) )
assume x in the carrier of (Ort_Comp W) ; :: thesis: x in the carrier of (Ort_Comp M)
then x in { v where v is VECTOR of V : for w being VECTOR of V st w in W holds
w,v are_orthogonal } by Def3;
then consider v being VECTOR of V such that
A4: ( x = v & ( for w being VECTOR of V st w in W holds
w,v are_orthogonal ) ) ;
for w being VECTOR of V st w in M holds
w,v are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in M implies w,v are_orthogonal )
assume w in M ; :: thesis: w,v are_orthogonal
then w in W by A1, STRUCT_0:def 5;
hence w,v are_orthogonal by A4; :: thesis: verum

end;

then x in { v1 where v1 is VECTOR of V : for w being VECTOR of V st w in M holds
w,v1 are_orthogonal } by A4;
hence x in the carrier of (Ort_Comp M) by Def4; :: thesis: verum

end;

then the carrier of (Ort_Comp W) c= the carrier of (Ort_Comp M) by TARSKI:def 3;
then the carrier of (Ort_Comp W) = the carrier of (Ort_Comp M) by A3, XBOOLE_0:def 10;
hence Ort_Comp M = Ort_Comp W by RUSUB_1:24; :: thesis: verum