let AFV be WeakAffVect; :: thesis: for q, p, a being Element of AFV holds PSym q,(PSym p,(PSym q,a)) = PSym (PSym q,p),a
let q, p, a be Element of AFV; :: thesis: PSym q,(PSym p,(PSym q,a)) = PSym (PSym q,p),a
Mid PSym q,a,p, PSym p,(PSym q,a) by Def4;
then Mid PSym q,(PSym q,a), PSym q,p, PSym q,(PSym p,(PSym q,a)) by Th42;
then PSym q,(PSym p,(PSym q,a)) = PSym (PSym q,p),(PSym q,(PSym q,a)) by Def4;
hence PSym q,(PSym p,(PSym q,a)) = PSym (PSym q,p),a by Th36; :: thesis: verum