let V be RealLinearSpace; :: thesis: for v being VECTOR of V st v = - v holds
v = 0. V
let v be VECTOR of V; :: thesis: ( v = - v implies v = 0. V )
assume v = - v ; :: thesis: v = 0. V
then 0. V = v + v by Def13
.= (1 * v) + v by Def11
.= (1 * v) + (1 * v) by Def11
.= (1 + 1) * v by Def9
.= 2 * v ;
hence v = 0. V by Th24; :: thesis: verum