[:NAT ,NAT :],[:[:NAT ,NAT :],NAT :] are_equipotent by Th53, CARD_2:15;
then A1: NAT ,[:[:NAT ,NAT :],NAT :] are_equipotent by Th53, WELLORD2:22;
[:[: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, WELLORD2:def 4;
deffunc H₁( set ) -> set = F₁((((N . $1) `1 ) `1 ),(((N . $1) `1 ) `2 ),((N . $1) `2 ));
consider f being Function such that
A4: ( dom f = NAT & ( for x being set st x in NAT holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
{ F₁(n1,n2,n3) where n1, n2, n3 is Element of NAT : P₁[n1,n2,n3] } c= rng f

proof

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

end;

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