for V being Z_Module st (Omega). V is free holds
V is free