theorem :: GROUP_19:42

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
for i being Element of I
for f being Element of (F . i)
for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)