:: deftheorem Def5 defines Padd AFVECT0:def 5 :
for AFV being WeakAffVect
for o, a, b, b₅ being Element of AFV holds
( b₅ = Padd (o,a,b) iff o,a // b,b₅ );