let AFV be WeakAffVect; :: thesis: for o being Element of
for a, b being Element of holds a + b = b + a
let o be Element of ; :: thesis: for a, b being Element of holds a + b = b + a
let a, b be Element of ; :: thesis: a + b = b + a
reconsider a' = a, b' = b as Element of ;
reconsider c' = a + b as Element of ;
c' = Padd o,a',b' by Def7;
then o,a' // b',c' by Def5;
then o,b' // a',c' by Def1;
then c' = Padd o,b',a' by Def5
.= b + a by Def7 ;
hence a + b = b + a ; :: thesis: verum