:: deftheorem Def1 defines "" EQUATION:def 1 :
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 object st i in I holds
b₄ . i = (F . i) " (A . i) );