for V being RealLinearSpace
for M being non empty Subset of V holds 0 * M = {(0. V)} by Lm2;