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

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

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

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

end;

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

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

end;

end;