let I, J be non empty set ; :: thesis: for a being Function of I,J
for F being multMagma-Family of J holds trans_prod (F,a) is multiplicative
let a be Function of I,J; :: thesis: for F being multMagma-Family of J holds trans_prod (F,a) is multiplicative
let F be multMagma-Family of J; :: thesis: trans_prod (F,a) is multiplicative
reconsider f = trans_prod (F,a) as Function of (product F),(product (F * a)) ;
for x, y being Element of (product F) holds f . (x * y) = (f . x) * (f . y)

proof

let x, y be Element of (product F); :: thesis: f . (x * y) = (f . x) * (f . y)
A1: f . (x * y) = (x * y) * a by Def2;
A2: f . x = x * a by Def2;
x * a in product (F * a) by Th1;
then reconsider xa = x * a as Element of (product (F * a)) ;
y * a in product (F * a) by Th1;
then reconsider ya = y * a as Element of (product (F * a)) ;
A3: dom (xa * ya) = I by GROUP_19:3;
A4: dom a = I by FUNCT_2:def 1;
dom (x * y) = J by GROUP_19:3;
then A5: rng a c= dom (x * y) ;
for i being object st i in I holds
(xa * ya) . i = ((x * y) * a) . i

proof

let i be object ; :: thesis: ( i in I implies (xa * ya) . i = ((x * y) * a) . i )
assume i in I ; :: thesis: (xa * ya) . i = ((x * y) * a) . i
then reconsider i = i as Element of I ;
reconsider Fai = (F * a) . i as multMagma ;
reconsider j = a . i as Element of J ;
reconsider Fj = F . j as multMagma ;
xa in product (F * a) ;
then xa . i in (F * a) . i by GROUP_19:5;
then reconsider xai = xa . i as Element of Fai ;
ya in product (F * a) ;
then ya . i in (F * a) . i by GROUP_19:5;
then reconsider yai = ya . i as Element of Fai ;
x in product F ;
then x . j in F . j by GROUP_19:5;
then reconsider xj = x . j as Element of Fj ;
y in product F ;
then y . j in F . j by GROUP_19:5;
then reconsider yj = y . j as Element of Fj ;
A6: xa . i = x . j by A4, FUNCT_1:13;
A7: ya . i = y . j by A4, FUNCT_1:13;
((x * y) * a) . i = (x * y) . j by A4, FUNCT_1:13
.= xj * yj by GROUP_7:1
.= xai * yai by A4, A6, A7, FUNCT_1:13
.= (xa * ya) . i by GROUP_7:1 ;
hence (xa * ya) . i = ((x * y) * a) . i ; :: thesis: verum

end;

then xa * ya = (x * y) * a by A3, A4, A5, RELAT_1:27;
hence f . (x * y) = (f . x) * (f . y) by A1, A2, Def2; :: thesis: verum

end;

hence trans_prod (F,a) is multiplicative by GROUP_6:def 6; :: thesis: verum