let G be Group; :: thesis: 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) )
let I be non empty set ; :: thesis: 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) )
let F be Group-Family of I; :: thesis: 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) )
let f be ManySortedSet of I; :: thesis: ( f is Homomorphism-Family of G,F iff for i being Element of I holds f . i is Homomorphism of G,(F . i) )
thus ( f is Homomorphism-Family of G,F implies for i being Element of I holds f . i is Homomorphism of G,(F . i) ) by Def10; :: thesis: ( ( for i being Element of I holds f . i is Homomorphism of G,(F . i) ) implies f is Homomorphism-Family of G,F )
assume A1: for i being Element of I holds f . i is Homomorphism of G,(F . i) ; :: thesis: f is Homomorphism-Family of G,F
for i being object st i in dom f holds
f . i is Function by A1;
then f is Function-yielding by FUNCOP_1:def 6;
hence f is Homomorphism-Family of G,F by A1, Def10; :: thesis: verum