:: deftheorem Def6 defines Padd AFVECT0:def 6 :
for AFV being WeakAffVect
for o being Element of AFV
for b₃ being BinOp of the carrier of AFV holds
( b₃ = Padd o iff for a, b being Element of AFV holds b₃ . (a,b) = Padd (o,a,b) );