let AFV be WeakAffVect; :: thesis: for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a
let o be Element of AFV; :: thesis: for a being Element of (GroupVect (AFV,o)) holds a + (0. (GroupVect (AFV,o))) = a
let a be Element of (GroupVect (AFV,o)); :: thesis: a + (0. (GroupVect (AFV,o))) = a
reconsider a9 = a as Element of AFV ;
reconsider x9 = a + (0. (GroupVect (AFV,o))) as Element of AFV ;
x9 = Padd (o,a9,o) by Def6;
then o,a9 // o,x9 by Def5;
hence a + (0. (GroupVect (AFV,o))) = a by Th4; :: thesis: verum