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