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;
F is sequence of RAT by A2, FUNCT_2:2;
hence ex F being sequence of RAT st
( F is one-to-one & dom F = NAT & rng F = RAT ) by A1, A2; :: thesis: verum