let V be free finite-rank Z_Module; :: thesis: rank ((0). V) = 0
(Omega). ((0). V) = (0). ((0). V) by ZMODUL01:51;
hence rank ((0). V) = 0 by RL5Th33; :: thesis: verum