:: deftheorem Def16 defines ProductHom GROUP_21:def 16 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for G being Group
for M being DirectSumComponents of G,I
for N being Group-Family of I,J
for h being ManySortedSet of I st ( for i being Element of I ex hi being Homomorphism of ((sum_bundle N) . i),(M . i) st
( hi = h . i & hi is bijective ) ) holds
for b₇ being Homomorphism of (dsum N),(sum M) holds
( b₇ = ProductHom (G,M,N,h) iff ( b₇ = SumMap ((sum_bundle N),M,h) & b₇ is bijective ) );