for v being Element of F_Rat
for v1 being Rational st v = v1 holds
for n being Nat holds (Nat-mult-left F_Rat) . (n,v) = n * v1