let V be Z_Module; :: thesis: for l being Z_Linear_Combination of {} the carrier of V holds l = Z_ZeroLC V
let l be Z_Linear_Combination of {} the carrier of V; :: thesis: l = Z_ZeroLC V
Carrier l c= {} by Def21;
then Carrier l = {} ;
hence l = Z_ZeroLC V by Def20; :: thesis: verum