theorem :: AFVECT0:41

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