:: deftheorem Def11 defines Homomorphism-Family GROUP_23:def 11 :
for I being non empty set
for F1, F2 being Group-Family of I
for b₄ being ManySortedFunction of F1,F2 holds
( b₄ is Homomorphism-Family of F1,F2 iff for i being Element of I holds b₄ . i is Homomorphism of (F1 . i),(F2 . i) );