theorem Th5: :: GROUP_21:7

for I, J being non empty set
for F being multMagma-Family of J
for a being Function of I,J st a is bijective holds
( dom (trans_prod (F,a)) = [#] (product F) & rng (trans_prod (F,a)) = [#] (product (F * a)) )