:: deftheorem Def2 defines trans_prod GROUP_21:def 2 :
for I, J being non empty set
for a being Function of I,J
for F being multMagma-Family of J
for b₅ being Function of (product F),(product (F * a)) holds
( b₅ = trans_prod (F,a) iff for x being Element of (product F) holds b₅ . x = x * a );