:: deftheorem defines (Funcs) PBOOLE:def 17 :
for I being set
for X, Y, b₄ being ManySortedSet of I holds
( b₄ = (Funcs) (X,Y) iff for i being object st i in I holds
b₄ . i = Funcs ((X . i),(Y . i)) );