deffunc H₁( Element of I) -> Homomorphism of (H . $1),G = the Homomorphism of (H . $1),G;
consider f being ManySortedSet of I such that
A1: for i being Element of I holds f . i = H₁(i) from PBOOLE:sch 5();

now :: thesis: for x being object st x in dom f holds
f . x is Function

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 . x = the Homomorphism of (H . i),G by A1;
hence f . x is Function ; :: thesis: verum

end;

then reconsider f = f as Function-yielding ManySortedSet of I by FUNCOP_1:def 6;
take f ; :: thesis: for i being Element of I holds f . i is Homomorphism of (H . i),G

now :: thesis: for i being Element of I holds f . i is Homomorphism of (H . i),G

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

end;

hence for i being Element of I holds f . i is Homomorphism of (H . i),G ; :: thesis: verum