let AFV be WeakAffVect; :: thesis: for o being Element of AFV
for a, b being Element of (GroupVect AFV,o) holds a + b = b + a
let o be Element of AFV; :: thesis: for a, b being Element of (GroupVect AFV,o) holds a + b = b + a
let a, b be Element of (GroupVect AFV,o); :: thesis: a + b = b + a
reconsider a' = a, b' = b as Element of AFV ;
reconsider c' = a + b as Element of AFV ;
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