let V be RealUnitarySpace; :: thesis: Ort_Comp ((0). V) = (Omega). V
for x being object st x in the carrier of ((Omega). V) holds
x in the carrier of (Ort_Comp ((0). V))

proof

let x be object ; :: thesis: ( x in the carrier of ((Omega). V) implies x in the carrier of (Ort_Comp ((0). V)) )
assume x in the carrier of ((Omega). V) ; :: thesis: x in the carrier of (Ort_Comp ((0). V))
then x in (Omega). V ;
then x in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) by RUSUB_1:def 3;
then reconsider x = x as Element of V ;
for w being VECTOR of V st w in (0). V holds
w,x are_orthogonal

proof

let w be VECTOR of V; :: thesis: ( w in (0). V implies w,x are_orthogonal )
assume w in (0). V ; :: thesis: w,x are_orthogonal
then w in the carrier of ((0). V) ;
then w in {(0. V)} by RUSUB_1:def 2;
then w .|. x = (0. V) .|. x by TARSKI:def 1
.= 0 by BHSP_1:14 ;
hence w,x are_orthogonal by BHSP_1:def 3; :: thesis: verum

end;

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

end;

then A1: the carrier of ((Omega). V) c= the carrier of (Ort_Comp ((0). V)) ;
for x being object st x in the carrier of (Ort_Comp ((0). V)) holds
x in the carrier of ((Omega). V)

proof

let x be object ; :: thesis: ( x in the carrier of (Ort_Comp ((0). V)) implies x in the carrier of ((Omega). V) )
assume x in the carrier of (Ort_Comp ((0). V)) ; :: thesis: x in the carrier of ((Omega). V)
then x in Ort_Comp ((0). V) ;
then x in V by RUSUB_1:2;
then x in the carrier of V ;
then x in UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) ;
then x in (Omega). V by RUSUB_1:def 3;
hence x in the carrier of ((Omega). V) ; :: thesis: verum

end;

then the carrier of (Ort_Comp ((0). V)) c= the carrier of ((Omega). V) ;
then the carrier of ((Omega). V) = the carrier of (Ort_Comp ((0). V)) by A1;
hence Ort_Comp ((0). V) = (Omega). V by RUSUB_1:24; :: thesis: verum