for V being strict RealUnitarySpace holds V is Subspace of (Omega). V ;