theorem :: RUSUB_1:69

for V being RealUnitarySpace holds the carrier of V is Coset of (Omega). V