let AFV be WeakAffVect; :: thesis: for p, b being Element of AFV ex a being Element of AFV st PSym p,a = b
let p, b be Element of AFV; :: thesis: ex a being Element of AFV st PSym p,a = b
PSym p,(PSym p,b) = b by Th36;
hence ex a being Element of AFV st PSym p,a = b ; :: thesis: verum