for V being RealLinearSpace holds
( V is finite-dimensional iff (Omega). V is finite-dimensional )