theorem Th72: :: RUSUB_1:72

for V being RealUnitarySpace
for W being Subspace of V
for C being Coset of W
for u being VECTOR of V holds
( u in C iff C = u + W )