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