for V being non empty vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for M1, M2 being Subset of V
for z being Complex holds z * (M1 + M2) = (z * M1) + (z * M2)