let AFV be AffVect; :: thesis: for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) st a + a = 0. (GroupVect (AFV,o)) holds
a = 0. (GroupVect (AFV,o))
let o be Element of AFV; :: thesis: for a being Element of (GroupVect (AFV,o)) st a + a = 0. (GroupVect (AFV,o)) holds
a = 0. (GroupVect (AFV,o))
let a be Element of (GroupVect (AFV,o)); :: thesis: ( a + a = 0. (GroupVect (AFV,o)) implies a = 0. (GroupVect (AFV,o)) )
assume A1: a + a = 0. (GroupVect (AFV,o)) ; :: thesis: a = 0. (GroupVect (AFV,o))
reconsider a99 = a as Element of AFV ;
o = Padd (o,a99,a99) by A1, Def6;
then A2: o,a99 // a99,o by Def5;
o,o // o,o by Th1;
hence a = 0. (GroupVect (AFV,o)) by A2, TDGROUP:16; :: thesis: verum