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