let AFV be WeakAffVect; :: thesis: for a, b, p being Element of AFV st PSym (p,a) = PSym (p,b) holds
a = b
let a, b, p be Element of AFV; :: thesis: ( PSym (p,a) = PSym (p,b) implies a = b )
assume A1: PSym (p,a) = PSym (p,b) ; :: thesis: a = b
PSym (p,(PSym (p,a))) = a by Th29;
hence a = b by A1, Th29; :: thesis: verum