let AFV be WeakAffVect; :: thesis: for p, a, b being Element of AFV st PSym (p,a) = PSym (p,b) holds
a = b
let p, a, b 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 Th36;
hence a = b by A1, Th36; :: thesis: verum