let I, J be non empty set ; 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; for F being multMagma-Family of J holds trans_prod (F,a) is multiplicative
let F be multMagma-Family of J; 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)
hence
trans_prod (F,a) is multiplicative
by GROUP_6:def 6; verum