theorem Th30: :: AFVECT0:30

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