let V be ComplexLinearSpace; :: 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 RLVECT_1:15
.= v + v by RLVECT_1:17
.= (1r * v) + v by Def5
.= (1r * v) + (1r * v) by Def5
.= (1r + 1r) * v by Def3 ;
hence v = 0. V by Th2; :: thesis: verum