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 bijective
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 bijective
let F be Group-Family of J; :: thesis: ( a is bijective implies trans_sum (F,a) is bijective )
assume A1: a is bijective ; :: thesis: trans_sum (F,a) is bijective
reconsider f = trans_prod (F,a) as Homomorphism of (product F),(product (F * a)) ;
reconsider g = trans_sum (F,a) as Homomorphism of (sum F),(sum (F * a)) by A1, TT;
A2: g = f | (sum F) by A1, Def3;
f is bijective by A1, Th6;
then A3: g is one-to-one by A2, FUNCT_1:52;
for y being object st y in [#] (sum (F * a)) holds
y in rng g

proof

let y be object ; :: thesis: ( y in [#] (sum (F * a)) implies y in rng g )
assume A4: y in [#] (sum (F * a)) ; :: thesis: y in rng g
then reconsider y = y as Element of (product (F * a)) by GROUP_2:42;
set x = y * (a ");
y * (a ") in product F by A1, Th3;
then reconsider x = y * (a ") as Element of (product F) ;
A5: dom g = [#] (sum F) by FUNCT_2:def 1;
A6: ( dom x = J & dom y = I ) by GROUP_19:3;
then A7: y = x * a by A1, Th4;
y in sum (F * a) by A4;
then A8: x in sum F by A1, A6, A7, Th10;
y = f . x by A7, Def2;
then y = g . x by A2, A8, FUNCT_1:49;
hence y in rng g by A5, A8, FUNCT_1:def 3; :: thesis: verum

end;

then [#] (sum (F * a)) c= rng g ;
then g is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
hence trans_sum (F,a) is bijective by A3; :: thesis: verum