theorem Th9: :: GROUP_21:11

for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J
for x being Function st a is one-to-one & x in sum F holds
x * a in sum (F * a)