theorem TT: :: GROUP_21:14

for I, J being non empty set
for a being Function of I,J
for F being Group-Family of J st a is bijective holds
trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a))