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