set JA = J --> A;
set JB = J --> B;
for j being set st j in J holds
(J => f) . j is Function of (J --> A) . j,(J --> B) . j

proof

let j be set ; :: thesis: ( j in J implies (J => f) . j is Function of (J --> A) . j,(J --> B) . j )
assume A1: j in J ; :: thesis: (J => f) . j is Function of (J --> A) . j,(J --> B) . j
then ( (J --> A) . j = A & (J --> B) . j = B ) by FUNCOP_1:13;
hence (J => f) . j is Function of (J --> A) . j,(J --> B) . j by A1, FUNCOP_1:13; :: thesis: verum

end;

hence J => f is ManySortedFunction of J --> A,J --> B by PBOOLE:def 18; :: thesis: verum