for V being RealLinearSpace holds Up ((Omega). V) is circled