let I, J be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( a is bijective implies trans_sum (F,a) is Homomorphism of (sum F),(sum (F * a)) )
assume A1: a is bijective ; :: thesis: 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; :: thesis: verum