let R be Ring; :: thesis: for V being LeftMod of R
for v being Vector of V st v <> 0. V holds
not Lin {v} is trivial
let V be LeftMod of R; :: 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 MOD_3:7;
then (Omega). (Lin {v}) <> (0). (Lin {v}) by VECTSP_4:36;
hence not Lin {v} is trivial by ThTrivial1; :: thesis: verum