let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being LeftMod of GF holds {} the carrier of V is linearly-independent
let V be LeftMod of GF; :: thesis: {} the carrier of V is linearly-independent
let l be Linear_Combination of {} the carrier of V; :: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
Carrier l c= {} by VECTSP_6:def 4;
hence ( Sum l = 0. V implies Carrier l = {} ) ; :: thesis: verum