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, Def7;
then A2: o,a99 // a99,o by Def5;
o,o // o,o by Th2;
hence a = 0. (GroupVect AFV,o) by A2, TDGROUP:21; :: thesis: verum
set GV = GroupVect AFV,o;