let a be Integer; :: thesis: for V being Z_Module
for v, w being VECTOR of V st V is Mult-cancelable & a <> 0 & a * v = a * w holds
v = w
let V be Z_Module; :: thesis: for v, w being VECTOR of V st V is Mult-cancelable & a <> 0 & a * v = a * w holds
v = w
let v, w be VECTOR of V; :: thesis: ( V is Mult-cancelable & a <> 0 & a * v = a * w implies v = w )
assume A1: V is Mult-cancelable ; :: thesis: ( not a <> 0 or not a * v = a * w or v = w )
assume that
A2: a <> 0 and
A3: a * v = a * w ; :: thesis: v = w
0. V = (a * v) - (a * w) by A3, RLVECT_1:15
.= a * (v - w) by Th8 ;
then v - w = 0. V by A2, A1;
hence v = w by RLVECT_1:21; :: thesis: verum