theorem Th3: :: GROUP_21:5

for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J
for y being Element of (product (F * a)) st a is bijective holds
y * (a ") in product F