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_{1}( object ) -> set = F_{1}(((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_{1}(x) ) )
from FUNCT_1:sch 3();

{ F_{1}(n1,n2) where n1, n2 is Nat : P_{1}[n1,n2] } c= rng f
_{1}(n1,n2) where n1, n2 is Nat : P_{1}[n1,n2] } is countable
by A3, CARD_3:93; :: thesis: verum

N is one-to-one and

A1: dom N = NAT and

A2: rng N = [:NAT,NAT:] by Th5, WELLORD2:def 4;

deffunc H

consider f being Function such that

A3: ( dom f = NAT & ( for x being object st x in NAT holds

f . x = H

{ F

proof

hence
{ F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{1}(n1,n2) where n1, n2 is Nat : P_{1}[n1,n2] } or x in rng f )

assume x in { F_{1}(n1,n2) where n1, n2 is Nat : P_{1}[n1,n2] }
; :: thesis: x in rng f

then consider n1, n2 being Nat such that

A4: x = F_{1}(n1,n2)
and

P_{1}[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;assume x in { F

then consider n1, n2 being Nat such that

A4: x = F

P

( 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