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

let y be object ; :: thesis:
assume y in [#] (product (F * a)) ; :: thesis:
then reconsider y = y as Element of (product (F * a)) ;
set x = y * (a ");
y * (a ") in product F by A1, Th3;
then reconsider x = y * (a ") as Element of (product F) ;
( dom x = J & dom y = I ) by GROUP_19:3;
then y = x * a by A1, Th4;
then y = (trans_prod (F,a)) . x by Def2;
hence ex x being object st
( x in [#] (product F) & y = (trans_prod (F,a)) . x ) ; :: thesis:

end;