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 & PSym p,(PSym p,b) = b ) by Th36;
hence a = b by A1; :: thesis: verum