let K be Ring; :: thesis: for V being LeftMod of K
for A being Subset of V st not K is trivial & A is linearly-independent holds
not 0. V in A
let V be LeftMod of K; :: thesis: for A being Subset of V st not K is trivial & A is linearly-independent holds
not 0. V in A
let A be Subset of V; :: thesis: ( not K is trivial & A is linearly-independent implies not 0. V in A )
assume A1: ( not K is trivial & A is linearly-independent ) ; :: thesis: not 0. V in A
then 0. K <> 1_ K by LMOD_6:def 2;
hence not 0. V in A by A1, LMOD_5:3; :: thesis: verum