let I, J be non empty set ; :: thesis: for a being Function of I,J
for F being multMagma-Family of J st a is bijective holds
trans_prod (F,a) is bijective
let a be Function of I,J; :: thesis: for F being multMagma-Family of J st a is bijective holds
trans_prod (F,a) is bijective
let F be multMagma-Family of J; :: thesis: ( a is bijective implies trans_prod (F,a) is bijective )
assume A1: a is bijective ; :: thesis: trans_prod (F,a) is bijective
reconsider f = trans_prod (F,a) as Function of (product F),(product (F * a)) ;
A2: ( dom f = [#] (product F) & rng f = [#] (product (F * a)) ) by A1, Th5;
for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A3: x in dom f and
A4: y in dom f and
A5: f . x = f . y ; :: thesis: x = y
reconsider x = x as Element of (product F) by A3;
reconsider y = y as Element of (product F) by A4;
A6: ( dom x = J & dom y = J ) by GROUP_19:3;
A7: rng a = J by A1, FUNCT_2:def 3;
f . x = x * a by Def2;
then x * a = y * a by A5, Def2;
hence x = y by A6, A7, FUNCT_1:86; :: thesis: verum

end;

then A8: f is one-to-one ;
f is onto by A2, FUNCT_2:def 3;
hence trans_prod (F,a) is bijective by A8; :: thesis: verum