set JA = J --> A;
set JB = J --> B;
for j being object st j in J holds
(J => f) . j is Function of ((J --> A) . j),((J --> B) . j)
proof
let j be object ; :: 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:7;
hence (J => f) . j is Function of ((J --> A) . j),((J --> B) . j) by A1, FUNCOP_1:7; :: thesis: verum
end;
hence J => f is ManySortedFunction of J --> A,J --> B by PBOOLE:def 15; :: thesis: verum