:: deftheorem Def10 defines dprod2prod GROUP_21:def 10 :
for I being non empty set
for J being non-empty disjoint_valued ManySortedSet of I
for F being Group-Family of I,J
for b₄ being Homomorphism of (dprod F),(product (Union F)) holds
( b₄ = dprod2prod F iff for x being Element of (dprod F)
for i being Element of I holds x . i = (b₄ . x) | (J . i) );