theorem Th34: :: GROUP_1A:235
for G being addGroup
for A, B, C being Subset of G holds (A + B) * C c= (A * C) + (B * C)