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 that
A1: not K is trivial and
A2: A is linearly-independent ; :: thesis: not 0. V in A
0. K <> 1_ K by A1, LMOD_6:def 1;
then not K is degenerated ;
hence not 0. V in A by A2, VECTSP_7:2; :: thesis: verum