let V be Z_Module; :: thesis: for a being Element of INT.Ring
for v, w being Vector of V st V is Mult-cancelable & a <> 0. INT.Ring & a * v = a * w holds
v = w
let a be Element of INT.Ring; :: thesis: for v, w being Vector of V st V is Mult-cancelable & a <> 0. INT.Ring & a * v = a * w holds
v = w
let v, w be Vector of V; :: thesis: ( V is Mult-cancelable & a <> 0. INT.Ring & a * v = a * w implies v = w )
assume A1: V is Mult-cancelable ; :: thesis: ( not a <> 0. INT.Ring or not a * v = a * w or v = w )
set R = INT.Ring ;
assume that
A2: a <> 0. INT.Ring 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