let R be non degenerated Ring; :: thesis: for V being LeftMod of R
for A being Subset of V st A is linearly-independent holds
not 0. V in A
let V be LeftMod of R; :: thesis: for A being Subset of V st A is linearly-independent holds
not 0. V in A
let A be Subset of V; :: thesis: ( A is linearly-independent implies not 0. V in A )
assume that
A2: A is linearly-independent and
A3: 0. V in A ; :: thesis: contradiction
deffunc H₁( set ) -> Element of the carrier of R = 0. R;
consider f being Function of the carrier of V, the carrier of R such that
A4: f . (0. V) = 1. R and
A5: for v being Element of V st v <> 0. V holds
f . v = H₁(v) from FUNCT_2:sch 6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
ex T being finite Subset of V st
for v being Vector of V st not v in T holds
f . v = 0. R

proof

take T = {(0. V)}; :: thesis: for v being Vector of V st not v in T holds
f . v = 0. R
let v be Vector of V; :: thesis: ( not v in T implies f . v = 0. R )
assume not v in T ; :: thesis: f . v = 0. R
then v <> 0. V by TARSKI:def 1;
hence f . v = 0. R by A5; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
A6: Carrier f = {(0. V)}

proof

thus Carrier f c= {(0. V)} :: according to XBOOLE_0:def 10 :: thesis: {(0. V)} c= Carrier f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in {(0. V)} )
assume x in Carrier f ; :: thesis: x in {(0. V)}
then consider v being Vector of V such that
A7: v = x and
A8: f . v <> 0. R ;
v = 0. V by A5, A8;
hence x in {(0. V)} by A7, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. V)} or x in Carrier f )
assume x in {(0. V)} ; :: thesis: x in Carrier f
then x = 0. V by TARSKI:def 1;
hence x in Carrier f by A4; :: thesis: verum

end;

then Carrier f c= A by A3, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def 4;
Sum f = (f . (0. V)) * (0. V) by A6, VECTSP_6:20
.= 0. V by VECTSP_1:14 ;
hence contradiction by A2, A6; :: thesis: verum