let AFV be AffVect; 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; 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)); ( a + a = 0. (GroupVect (AFV,o)) implies a = 0. (GroupVect (AFV,o)) )
assume A1:
a + a = 0. (GroupVect (AFV,o))
; 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; verum