deffunc H₁() -> non empty set = I;
deffunc H₂( Element of I) -> Element of bool [: the carrier of G, the carrier of (F . $1):] = 1: (G,(F . $1));
consider f being ManySortedSet of H₁() such that
A1: for i being Element of H₁() holds f . i = H₂(i) from PBOOLE:sch 5();
for x being object st x in dom f holds
f . x is Function

proof

let x be object ; :: thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; :: thesis: f . x is Function
then reconsider i = x as Element of I ;
f . i = 1: (G,(F . i)) by A1;
hence f . x is Function ; :: thesis: verum

end;

then reconsider f = f as ManySortedFunction of I by FUNCOP_1:def 6;
take f ; :: thesis: for i being Element of I holds f . i is Homomorphism of G,(F . i)
thus for i being Element of I holds f . i is Homomorphism of G,(F . i) :: thesis: verum

proof

let i be Element of I; :: thesis: f . i is Homomorphism of G,(F . i)
f . i = 1: (G,(F . i)) by A1;
hence f . i is Homomorphism of G,(F . i) ; :: thesis: verum

end;