deffunc H₁( Element of n -tuples_on RAT) -> set = n . 1;
consider f being Function such that
A1: ( dom f = n -tuples_on RAT & ( for d being Element of n -tuples_on RAT holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
for y being object holds
( y in f .: (n -tuples_on RAT) iff y in RAT )

proof

let y be object ; :: thesis: ( y in f .: (n -tuples_on RAT) iff y in RAT )
0 + 1 < n + 1 by XREAL_1:6;
then A2: 1 <= n by NAT_1:13;
then A3: 1 in Seg n ;

hereby :: thesis: ( y in RAT implies y in f .: (n -tuples_on RAT) )

assume y in f .: (n -tuples_on RAT) ; :: thesis: y in RAT
then consider x being object such that
A4: ( x in dom f & x in n -tuples_on RAT & y = f . x ) by FUNCT_1:def 6;
reconsider x = x as Element of n -tuples_on RAT by A4;
A5: y = x . 1 by A1, A4;
x in Funcs ((Seg n),RAT) by A4, FINSEQ_2:93;
then consider f1 being Function such that
A6: ( x = f1 & dom f1 = Seg n & rng f1 c= RAT ) by FUNCT_2:def 2;
thus y in RAT by A3, A5, A6, FUNCT_1:3; :: thesis: verum

end;

assume y in RAT ; :: thesis: y in f .: (n -tuples_on RAT)
then A7: {y} c= RAT by ZFMISC_1:31;
set x = (Seg n) --> y;
A8: ( dom ((Seg n) --> y) = Seg n & rng ((Seg n) --> y) c= {y} ) by FUNCOP_1:13;
rng ((Seg n) --> y) c= RAT by A7;
then (Seg n) --> y in Funcs ((Seg n),RAT) by A8, FUNCT_2:def 2;
then reconsider x = (Seg n) --> y as Element of n -tuples_on RAT by FINSEQ_2:93;
f . x = x . 1 by A1
.= y by A2, FINSEQ_1:1, FUNCOP_1:7 ;
hence y in f .: (n -tuples_on RAT) by A1, FUNCT_1:def 6; :: thesis: verum

end;

hence not RAT n is finite by TARSKI:2; :: thesis: verum