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)

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

hence
J => f is ManySortedFunction of J --> A,J --> B
by PBOOLE:def 15; :: thesis: verum
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;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