theorem :: GROUP_21:20

for I, J being non empty set
for G being Group
for x being finite-support Function of I,G
for y being finite-support Function of J,G
for a being Function of I,J st a is bijective & x = y * a & ( for i, j being Element of I holds (x . i) * (x . j) = (x . j) * (x . i) ) holds
Product x = Product y