theorem LMTFRat2: :: ZMODUL07:15

for x being Integer
for v being Element of F_Rat
for v1 being Rational st v = v1 holds
(Int-mult-left F_Rat) . (x,v) = x * v1