theorem ThRHom: :: GROUP_23:30

for G being Group
for I being non empty set
for F being Group-Family of I
for f being ManySortedSet of I holds
( f is Homomorphism-Family of G,F iff for i being Element of I holds f . i is Homomorphism of G,(F . i) )