for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V ex C being Coset of W st v in C by Lm17;