theorem :: ZMODUL05:17

for V being free Z_Module st [#] V is finite holds
(Omega). V = (0). V