let V be trivial Z_Module; :: thesis: (Omega). V = (0). V
assume (Omega). V <> (0). V ; :: thesis: contradiction
then consider v being VECTOR of V such that
A1: ( v in (Omega). V & v <> 0. V ) by ZMODUL04:24;
reconsider v = v as VECTOR of V ;
not V is trivial by A1;
hence contradiction ; :: thesis: verum