[:NAT,NAT:],[:[:NAT,NAT:],NAT:] are_equipotent by Th53, CARD_2:8;
then A1: NAT ,[:[:NAT,NAT:],NAT:] are_equipotent by Th53, 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, 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:43, MCART_1:46;
A7: ( [n1,n2,n3] `2 = ([n1,n2,n3] `1) `2 & [n1,n2,n3] `3 = [n1,n2,n3] `2 ) by MCART_1:46;
consider y being set such that
A8: y in dom N and
A9: [n1,n2,n3] = N . y by A3, FUNCT_1:def 3;
( [n1,n2,n3] `1 = n1 & [n1,n2,n3] `2 = n2 ) by MCART_1:43;
then x = f . y by A2, A4, A5, A8, A9, A6, A7;
hence x in rng f by A2, A4, A8, FUNCT_1:def 3; :: 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:93; :: thesis: verum