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:28
.= v + v by RLVECT_1:30
.= (1r * v) + v by Def2
.= (1r * v) + (1r * v) by Def2
.= (1r + 1r ) * v by Def2 ;
hence v = 0. V by Th3; :: thesis: verum