let I be non empty set ; :: thesis: for i being Element of I
for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F holds [i,(f . i)] in f
let i be Element of I; :: thesis: for F being Group-Family of I
for G being Group
for f being Homomorphism-Family of G,F holds [i,(f . i)] in f
let F be Group-Family of I; :: thesis: for G being Group
for f being Homomorphism-Family of G,F holds [i,(f . i)] in f
let G be Group; :: thesis: for f being Homomorphism-Family of G,F holds [i,(f . i)] in f
let f be Homomorphism-Family of G,F; :: thesis: [i,(f . i)] in f
( i in I & f is ManySortedSet of I ) ;
then i in dom f by PARTFUN1:def 2;
hence [i,(f . i)] in f by FUNCT_1:def 2; :: thesis: verum