let V be Z_Module; :: thesis: for a, b being Element of INT.Ring
for v being Vector of V st V is Mult-cancelable & v <> 0. V & a * v = b * v holds
a = b
let a, b be Element of INT.Ring; :: thesis: for v being Vector of V st V is Mult-cancelable & v <> 0. V & a * v = b * v holds
a = b
let v be Vector of V; :: thesis: ( V is Mult-cancelable & v <> 0. V & a * v = b * v implies a = b )
assume A1: V is Mult-cancelable ; :: thesis: ( not v <> 0. V or not a * v = b * v or a = b )
assume that
A2: v <> 0. V and
A3: a * v = b * v ; :: thesis: a = b
0. V = (a * v) - (b * v) by A3, RLVECT_1:15
.= (a - b) * v by Th9 ;
then (- b) + a = 0 by A2, A1
.= 0. INT.Ring ;
hence a = b ; :: thesis: verum