:: deftheorem defines .:.: PBOOLE:def 20 :
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b₄ being ManySortedSet of I holds
( b₄ = F .:.: A iff for i being set st i in I holds
b₄ . i = (F . i) .: (A . i) );