let R be Ring; :: thesis: for V being LeftMod of R
for v being Vector of V st not R is degenerated & V is Mult-cancelable holds
( {v} is linearly-independent iff v <> 0. V )

let V be LeftMod of R; :: thesis: for v being Vector of V st not R is degenerated & V is Mult-cancelable holds
( {v} is linearly-independent iff v <> 0. V )

let v be Vector of V; :: thesis: ( not R is degenerated & V is Mult-cancelable implies ( {v} is linearly-independent iff v <> 0. V ) )
assume A1: ( not R is degenerated & V is Mult-cancelable ) ; :: thesis: ( {v} is linearly-independent iff v <> 0. V )
thus ( {v} is linearly-independent implies v <> 0. V ) :: thesis: ( v <> 0. V implies {v} is linearly-independent )
proof end;
assume A2: v <> 0. V ; :: thesis:
let l be Linear_Combination of {v}; :: according to VECTSP_7:def 1 :: thesis: ( not Sum l = 0. V or Carrier l = {} )
A3: Carrier l c= {v} by VECTSP_6:def 4;
assume A4: Sum l = 0. V ; :: thesis:
now :: thesis:
per cases ( Carrier l = {} or Carrier l = {v} ) by ;
suppose A5: Carrier l = {v} ; :: thesis:
then A6: 0. V = (l . v) * v by ;
now :: thesis: not v in Carrier l
assume v in Carrier l ; :: thesis: contradiction
then ex u being Vector of V st
( v = u & l . u <> 0. R ) ;
hence contradiction by A2, A6, A1; :: thesis: verum
end;
hence Carrier l = {} by ; :: thesis: verum
end;
end;
end;
hence Carrier l = {} ; :: thesis: verum