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 )
set a = 1. INT.Ring;
assume v = - v ; :: thesis: v = 0. V
then 0. V = v + v by RLVECT_1:def 10
.= ((1. INT.Ring) * v) + v by VECTSP_1:def 17
.= ((1. INT.Ring) * v) + ((1. INT.Ring) * v) by VECTSP_1:def 17
.= ((1. INT.Ring) + (1. INT.Ring)) * v by VECTSP_1:def 15 ;
hence v = 0. V by A1; :: thesis: verum