let x, v be Element of INT.Ring; :: thesis: for v1 being Integer st v = v1 holds
(Int-mult-left INT.Ring) . (x,v) = x * v1
let v1 be Integer; :: thesis: ( v = v1 implies (Int-mult-left INT.Ring) . (x,v) = x * v1 )
assume A1: v = v1 ; :: thesis: (Int-mult-left INT.Ring) . (x,v) = x * v1
reconsider xx = x as Element of INT ;

per cases ( x >= 0 or x < 0 ) ;

suppose C1: x >= 0 ; :: thesis: (Int-mult-left INT.Ring) . (x,v) = x * v1

then reconsider x0 = x as Element of NAT by INT_1:3;
thus (Int-mult-left INT.Ring) . (x,v) = (Nat-mult-left INT.Ring) . (xx,v) by C1, ZMODUL01:def 20
.= (Nat-mult-left INT.Ring) . (x0,v)
.= x0 * v1 by LMINTRNG1, A1
.= x * v1 ; :: thesis: verum

end;

suppose C2: x < 0 ; :: thesis: (Int-mult-left INT.Ring) . (x,v) = x * v1

then reconsider x0 = - x as Element of NAT by INT_1:3;
thus (Int-mult-left INT.Ring) . (x,v) = (Nat-mult-left INT.Ring) . ((- x),(- v)) by C2, ZMODUL01:def 20
.= x0 * (- v1) by LMINTRNG1, A1
.= x * v1 ; :: thesis: verum

end;

end;