theorem :: AFVECT0:31

for AFV being WeakAffVect
for b, p being Element of AFV ex a being Element of AFV st PSym (p,a) = b