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

proof

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

end;

hence { F₁(n1,n2) where n1, n2 is Nat : P₁[n1,n2] } is countable by A3, CARD_3:93; :: thesis: verum