let V be Z_Module; :: thesis: for A being Subset of V holds Z_ZeroLC V is Z_Linear_Combination of A
let A be Subset of V; :: thesis: Z_ZeroLC V is Z_Linear_Combination of A
( Carrier (Z_ZeroLC V) = {} & {} c= A ) by Def20;
hence Z_ZeroLC V is Z_Linear_Combination of A by Def21; :: thesis: verum