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 Def6;
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 Def6 ;
hence a + b = b + a ; :: thesis: verum