[:NAT,NAT:],[:[:NAT,NAT:],NAT:] are_equipotent
by Th5, CARD_2:8;

then A1: NAT ,[:[:NAT,NAT:],NAT:] are_equipotent by Th5, WELLORD2:15;

[:[:NAT,NAT:],NAT:] = [:NAT,NAT,NAT:] by ZFMISC_1:def 3;

then consider N being Function such that

N is one-to-one and

A2: dom N = NAT and

A3: rng N = [:NAT,NAT,NAT:] by A1;

deffunc H_{1}( object ) -> set = F_{1}((((N . $1) `1) `1),(((N . $1) `1) `2),((N . $1) `2));

consider f being Function such that

A4: ( 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,n3) where n1, n2, n3 is Nat : P_{1}[n1,n2,n3] } c= rng f
_{1}(n1,n2,n3) where n1, n2, n3 is Nat : P_{1}[n1,n2,n3] } is countable
by A4, CARD_3:93; :: thesis: verum

then A1: NAT ,[:[:NAT,NAT:],NAT:] are_equipotent by Th5, WELLORD2:15;

[:[:NAT,NAT:],NAT:] = [:NAT,NAT,NAT:] by ZFMISC_1:def 3;

then consider N being Function such that

N is one-to-one and

A2: dom N = NAT and

A3: rng N = [:NAT,NAT,NAT:] by A1;

deffunc H

consider f being Function such that

A4: ( 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,n3) where n1, n2, n3 is Nat : P_{1}[n1,n2,n3] } or x in rng f )

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

then consider n1, n2, n3 being Nat such that

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

P_{1}[n1,n2,n3]
;

reconsider n1 = n1, n2 = n2, n3 = n3 as Element of NAT by ORDINAL1:def 12;

A6: ( [n1,n2,n3] `3_3 = n3 & [n1,n2,n3] `1_3 = ([n1,n2,n3] `1) `1 ) ;

consider y being object such that

A7: y in dom N and

A8: [n1,n2,n3] = N . y by A3, FUNCT_1:def 3;

( [n1,n2,n3] `1_3 = n1 & [n1,n2,n3] `2_3 = n2 ) ;

then x = f . y by A2, A4, A5, A7, A8, A6;

hence x in rng f by A2, A4, A7, FUNCT_1:def 3; :: thesis: verum

end;assume x in { F

then consider n1, n2, n3 being Nat such that

A5: x = F

P

reconsider n1 = n1, n2 = n2, n3 = n3 as Element of NAT by ORDINAL1:def 12;

A6: ( [n1,n2,n3] `3_3 = n3 & [n1,n2,n3] `1_3 = ([n1,n2,n3] `1) `1 ) ;

consider y being object such that

A7: y in dom N and

A8: [n1,n2,n3] = N . y by A3, FUNCT_1:def 3;

( [n1,n2,n3] `1_3 = n1 & [n1,n2,n3] `2_3 = n2 ) ;

then x = f . y by A2, A4, A5, A7, A8, A6;

hence x in rng f by A2, A4, A7, FUNCT_1:def 3; :: thesis: verum