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

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