:: deftheorem Def7 defines SumMap GROUP_19:def 7 :

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

SumMap (F,G,h) = (ProductMap (F,G,h)) | (sum F);

for I being non empty set

for F, G being Group-Family of I

for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds

SumMap (F,G,h) = (ProductMap (F,G,h)) | (sum F);