theorem Th29: :: AFVECT0:29

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