:: deftheorem Def8 defines Homomorphism-Family GR_FREE0:def 8 :
for I being non empty set
for H being Group-like associative multMagma-Family of I
for G being Group
for b₄ being Function-yielding ManySortedSet of I holds
( b₄ is Homomorphism-Family of H,G iff for i being Element of I holds b₄ . i is Homomorphism of (H . i),G );