set V = the non trivial Z_Module;
(Omega). the non trivial Z_Module <> (0). the non trivial Z_Module ;
then consider v being Vector of the non trivial Z_Module such that
A1: ( v in (Omega). the non trivial Z_Module & v <> 0. the non trivial Z_Module ) by ZMODUL04:24;
take Lin {v} ; :: thesis: not Lin {v} is trivial
thus not Lin {v} is trivial by A1, ThTrivial2; :: thesis: verum