theorem Th1: :: GROUP_21:3

for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J
for x being Element of (product F) holds x * a in product (F * a)