:: deftheorem Def3 defines trans_sum GROUP_21:def 3 :
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) = (trans_prod (F,a)) | (sum F);