let R be Ring; :: thesis: for V being RightMod of R holds {} the carrier of V is linearly-independent
let V be RightMod of R; :: thesis: {} the carrier of V is linearly-independent
let l be Linear_Combination of {} the carrier of V; :: according to RMOD_4:def 13 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
Carrier l c= {} by Def5;
hence ( Sum l = 0. V implies Carrier l = {} ) ; :: thesis: verum