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

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