:: deftheorem Def15 defines ManySortedFunction PBOOLE:def 15 :
for I being set
for A, B, b₄ being ManySortedSet of I holds
( b₄ is ManySortedFunction of A,B iff for i being object st i in I holds
b₄ . i is Function of (A . i),(B . i) );