let V be Z_Module; :: thesis: for v being VECTOR of V st v <> 0. V holds
not Lin {v} is trivial
let v be VECTOR of V; :: thesis: ( v <> 0. V implies not Lin {v} is trivial )
assume A1: v <> 0. V ; :: thesis: not Lin {v} is trivial
{v} <> {(0. V)} by A1, ZFMISC_1:3;
then Lin {v} <> (0). V by ZMODUL02:68;
then (Omega). (Lin {v}) <> (0). (Lin {v}) by ZMODUL01:51;
hence not Lin {v} is trivial by ThTrivial1; :: thesis: verum