:: deftheorem Def6 defines -' PRE_POLY:def 6 :
for X being set
for b1, b2 being natural-valued ManySortedSet of X
for b₄ being ManySortedSet of X holds
( b₄ = b1 -' b2 iff for x being object holds b₄ . x = (b1 . x) -' (b2 . x) );