theorem Th23: :: RAT_1:26

for m being Integer
for p being Rational st m <> 0 holds
p = ((numerator p) * m) / ((denominator p) * m)