consider N being Function such that
N is one-to-one and
A1: dom N = NAT and
A2: rng N = [:NAT ,NAT :] by Th53, WELLORD2:def 4;
deffunc H₁( set ) -> set = F₁(((N . $1) `1 ),((N . $1) `2 ));
consider f being Function such that
A3: ( dom f = NAT & ( for x being set st x in NAT holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
{ F₁(n1,n2) where n1, n2 is Element of NAT : P₁[n1,n2] } c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₁(n1,n2) where n1, n2 is Element of NAT : P₁[n1,n2] } or x in rng f )
assume x in { F₁(n1,n2) where n1, n2 is Element of NAT : P₁[n1,n2] } ; :: thesis: x in rng f
then consider n1, n2 being Element of NAT such that
A4: x = F₁(n1,n2) and
P₁[n1,n2] ;
consider y being set such that
A5: y in dom N and
A6: [n1,n2] = N . y by A2, FUNCT_1:def 5;
( [n1,n2] `1 = n1 & [n1,n2] `2 = n2 ) by MCART_1:7;
then x = f . y by A1, A3, A4, A5, A6;
hence x in rng f by A1, A3, A5, FUNCT_1:def 5; :: thesis: verum

end;

hence { F₁(n1,n2) where n1, n2 is Element of NAT : P₁[n1,n2] } is countable by A3, CARD_3:127; :: thesis: verum