consider F being Function such that
A1:
F is one-to-one
and
A2:
( dom F = NAT & rng F = RAT )
by MESFUNC1:5, WELLORD2:def 4;
A3:
F is Function of NAT ,RAT
by A2, FUNCT_2:4;
thus
ex F being Function of NAT ,RAT st
( F is one-to-one & dom F = NAT & rng F = RAT )
by A1, A2, A3; verum