:: deftheorem Def10 defines Homomorphism-Family GROUP_23:def 10 :
for G being Group
for I being non empty set
for F being Group-Family of I
for b₄ being ManySortedFunction of I holds
( b₄ is Homomorphism-Family of G,F iff for i being Element of I holds b₄ . i is Homomorphism of G,(F . i) );