[: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₁( object ) -> 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 object st x in NAT holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
{ F₁(n1,n2,n3) where n1, n2, n3 is Nat : P₁[n1,n2,n3] } c= rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₁(n1,n2,n3) where n1, n2, n3 is Nat : P₁[n1,n2,n3] } or x in rng f )
assume x in { F₁(n1,n2,n3) where n1, n2, n3 is Nat : P₁[n1,n2,n3] } ; :: thesis: x in rng f
then consider n1, n2, n3 being Nat such that
A5: x = F₁(n1,n2,n3) and
P₁[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;

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