:: deftheorem Def15 defines InterHom GROUP_21:def 15 :
for I being non empty set
for G being Group
for F being internal DirectSumComponents of G,I
for b₄ being Homomorphism of (sum F),G holds
( b₄ = InterHom F iff ( b₄ is bijective & ( for x being finite-support Function of I,G st x in sum F holds
b₄ . x = Product x ) ) );