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