:: deftheorem Def5 defines + PRE_POLY:def 5 :
for X being set
for b1, b2 being complex-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) );