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