let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for G being Group
for F being Homomorphism-Family of H,G holds uncurry F is ManySortedSet of FreeAtoms H
let H be Group-like associative multMagma-Family of I; :: thesis: for G being Group
for F being Homomorphism-Family of H,G holds uncurry F is ManySortedSet of FreeAtoms H
let G be Group; :: thesis: for F being Homomorphism-Family of H,G holds uncurry F is ManySortedSet of FreeAtoms H
let F be Homomorphism-Family of H,G; :: thesis: uncurry F is ManySortedSet of FreeAtoms H

now :: thesis: for x being object holds
( ( x in FreeAtoms H implies x in dom (uncurry F) ) & ( x in dom (uncurry F) implies x in FreeAtoms H ) )

let x be object ; :: thesis: ( ( x in FreeAtoms H implies x in dom (uncurry F) ) & ( x in dom (uncurry F) implies x in FreeAtoms H ) )

hereby :: thesis: ( x in dom (uncurry F) implies x in FreeAtoms H )

assume A1: x in FreeAtoms H ; :: thesis: x in dom (uncurry F)
ex i being object ex g being Function ex y being object st
( x = [i,y] & i in dom F & g = F . i & y in dom g )

proof

consider i, y being object such that
A2: x = [i,y] by A1, RELAT_1:def 1;
i in dom H by A1, A2, Th7;
then reconsider i = i as Element of I ;
take i ; :: thesis: ex g being Function ex y being object st
( x = [i,y] & i in dom F & g = F . i & y in dom g )
take F . i ; :: thesis: ex y being object st
( x = [i,y] & i in dom F & F . i = F . i & y in dom (F . i) )
take y ; :: thesis: ( x = [i,y] & i in dom F & F . i = F . i & y in dom (F . i) )
A3: y in the carrier of (H . i) by A1, A2, Th9;
F . i is Homomorphism of (H . i),G by Def8;
then ( y in dom (F . i) & i in I ) by A3, FUNCT_2:def 1;
hence ( x = [i,y] & i in dom F & F . i = F . i & y in dom (F . i) ) by A2, PARTFUN1:def 2; :: thesis: verum

end;

hence x in dom (uncurry F) by FUNCT_5:def 2; :: thesis: verum

end;

assume x in dom (uncurry F) ; :: thesis: x in FreeAtoms H
then consider y being object , g being Function, z being object such that
A4: ( x = [y,z] & y in dom F & g = F . y & z in dom g ) by FUNCT_5:def 2;
reconsider i = y as Element of I by A4;
( g = F . i & F . i is Homomorphism of (H . i),G ) by A4, Def8;
then z in the carrier of (H . i) by A4, FUNCT_2:def 1;
hence x in FreeAtoms H by A4, Th9; :: thesis: verum

end;

then dom (uncurry F) = FreeAtoms H by TARSKI:2;
hence uncurry F is ManySortedSet of FreeAtoms H by PARTFUN1:def 2, RELAT_1:def 18; :: thesis: verum