let V be Z_Module; :: thesis: {} the carrier of V is linearly-independent
let l be Z_Linear_Combination of {} the carrier of V; :: according to ZMODUL02:def 36 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
Carrier l c= {} by Def21;
hence ( Sum l = 0. V implies Carrier l = {} ) ; :: thesis: verum