deffunc H₁( Element of I) -> Element of bool [: the carrier of (F1 . $1), the carrier of (F2 . $1):] = 1: ((F1 . $1),(F2 . $1));
consider phi being ManySortedSet of I such that
A1: for i being Element of I holds phi . i = H₁(i) from PBOOLE:sch 5();
A2: for i being Element of I holds phi . i is Homomorphism of (F1 . i),(F2 . i)

proof

let i be Element of I; :: thesis: phi . i is Homomorphism of (F1 . i),(F2 . i)
phi . i = 1: ((F1 . i),(F2 . i)) by A1;
hence phi . i is Homomorphism of (F1 . i),(F2 . i) ; :: thesis: verum

end;

for i being Element of I holds phi . i is Function of ((Carrier F1) . i),((Carrier F2) . i)

proof

let i be Element of I; :: thesis: phi . i is Function of ((Carrier F1) . i),((Carrier F2) . i)
( the carrier of (F1 . i) = (Carrier F1) . i & the carrier of (F2 . i) = (Carrier F2) . i ) by Th9;
hence phi . i is Function of ((Carrier F1) . i),((Carrier F2) . i) by A2; :: thesis: verum

end;

then reconsider phi = phi as ManySortedFunction of F1,F2 by Th25;
take phi ; :: thesis: for i being Element of I holds phi . i is Homomorphism of (F1 . i),(F2 . i)
thus for i being Element of I holds phi . i is Homomorphism of (F1 . i),(F2 . i) by A2; :: thesis: verum