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 object st x in the carrier of (Ort_Comp W) holds
x in the carrier of (Ort_Comp M)

proof

let x be object ; :: 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
A2: x = v and
A3: 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 by A1, STRUCT_0:def 5, A3;
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 A2;
hence x in the carrier of (Ort_Comp M) by Def4; :: thesis: verum

end;

then A4: the carrier of (Ort_Comp W) c= the carrier of (Ort_Comp M) ;
for x being object st x in the carrier of (Ort_Comp M) holds
x in the carrier of (Ort_Comp W)

proof

let x be object ; :: 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
A5: x = v and
A6: 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 by A1, A6;
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 A5;
hence x in the carrier of (Ort_Comp W) by Def3; :: thesis: verum

end;

then the carrier of (Ort_Comp M) c= the carrier of (Ort_Comp W) ;
then the carrier of (Ort_Comp W) = the carrier of (Ort_Comp M) by A4;
hence Ort_Comp M = Ort_Comp W by RUSUB_1:24; :: thesis: verum