let I, J be 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))
let a be 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))
let F be Group-Family of J; ( a is bijective implies trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a)) )
assume A1:
a is bijective
; trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a))
set f = trans_sum (F,a);
A2:
trans_sum (F,a) = (trans_prod (F,a)) | (sum F)
by A1, Def3;
rng (trans_sum (F,a)) c= [#] (sum (F * a))
;
hence
trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a))
by A2, Th11; verum