let V be Z_Module; :: thesis: for v being VECTOR of V st V is Mult-cancelable & v = - v holds
v = 0. V
let v be VECTOR of V; :: thesis: ( V is Mult-cancelable & v = - v implies v = 0. V )
assume A1: V is Mult-cancelable ; :: thesis: ( not v = - v or v = 0. V )
assume v = - v ; :: thesis: v = 0. V
then 0. V = v + v by RLVECT_1:def 10
.= (1 * v) + v by Def5
.= (1 * v) + (1 * v) by Def5
.= (1 + 1) * v by Def3
.= 2 * v ;
hence v = 0. V by A1; :: thesis: verum