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 a9 = a, b9 = b as Element of AFV ;
reconsider c9 = a + b as Element of AFV ;
c9 = Padd o,a9,b9 by Def7;
then o,a9 // b9,c9 by Def5;
then o,b9 // a9,c9 by Def1;
then c9 = Padd o,b9,a9 by Def5
.= b + a by Def7 ;
hence a + b = b + a ; :: thesis: verum