uncurry F is ManySortedSet of FreeAtoms H by Lm5;
then A1: dom (uncurry F) = FreeAtoms H by PARTFUN1:def 2;

now :: thesis: for p being object st p in rng (uncurry F) holds
p in the carrier of G

let p be object ; :: thesis: ( p in rng (uncurry F) implies p in the carrier of G )
assume p in rng (uncurry F) ; :: thesis: p in the carrier of G
then consider x being object such that
A2: ( x in dom (uncurry F) & (uncurry F) . x = p ) by FUNCT_1:def 3;
consider i being object , g being Function, y being object such that
A3: ( x = [i,y] & i in dom F & g = F . i & y in dom g ) by A2, FUNCT_5:def 2;
reconsider i = i as Element of I by A3;
A4: g = F . (x `1) by A3;
p = g . (x `2) by A2, A4, FUNCT_5:def 2
.= (F . i) . y by A3 ;
then A5: p in rng (F . i) by A3, FUNCT_1:3;
F . i is Homomorphism of (H . i),G by Def8;
then rng (F . i) c= the carrier of G by RELAT_1:def 19;
hence p in the carrier of G by A5; :: thesis: verum

end;

hence uncurry F is Function of (FreeAtoms H),G by A1, TARSKI:def 3, FUNCT_2:2; :: thesis: verum