theorem Th19: :: GROUP_20:18

for I being non empty set
for G being Group
for F being Subgroup-Family of I,G
for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a