theorem Th11: :: ZMODUL02:11

for V being Z_Module
for A being Subset of V holds ZeroLC V is Linear_Combination of A by VECTSP_6:5;