consider F being Function such that
A1: F is one-to-one and
A2: ( dom F = NAT & rng F = [:NAT,NAT:] ) by CARD_4:5, WELLORD2:def 4;
F is sequence of [:NAT,NAT:] by A2, FUNCT_2:1;
hence ex F being sequence of [:NAT,NAT:] st
( F is one-to-one & dom F = NAT & rng F = [:NAT,NAT:] ) by A1, A2; :: thesis: verum