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 bijective
let a be Function of I,J; 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; ( a is bijective implies trans_sum (F,a) is bijective )
assume A1:
a is bijective
; 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 ;
( y in [#] (sum (F * a)) implies y in rng g )
assume A4:
y in [#] (sum (F * a))
;
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;
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; verum