consider H being ManySortedSet of F₁() such that
A2: for i being Element of F₁() holds H . i = F₄(i) from PBOOLE:sch 5();
for i being Element of F₁() holds H . i is Homomorphism of (F₂() . i),(F₃() . i)

proof

let i be Element of F₁(); :: thesis: H . i is Homomorphism of (F₂() . i),(F₃() . i)
H . i = F₄(i) by A2;
hence H . i is Homomorphism of (F₂() . i),(F₃() . i) by A1; :: thesis: verum

end;

then reconsider H = H as Homomorphism-Family of F₂(),F₃() by ThHom;
take H ; :: thesis: for i being Element of F₁() holds H . i = F₄(i)
thus for i being Element of F₁() holds H . i = F₄(i) by A2; :: thesis: verum