for AFV being WeakAffVect
for a, p being Element of AFV holds PSym (p,(PSym (p,a))) = a