theorem :: RUSUB_1:66
for V being RealUnitarySpace
for v being VECTOR of V holds {v} is Coset of (0). V