let V be Z_Module; :: thesis: rank ((0). V) = 0
reconsider 0Vs = (Omega). ((0). V) as strict free finite-rank Z_Module ;
(Omega). 0Vs = (0). ((0). V) by ZMODUL01:51;
hence rank ((0). V) = 0 by ZMODUL05:1; :: thesis: verum