A1: the carrier of (TOP-REAL n) = REAL n by EUCLID:22
.= n -tuples_on REAL by EUCLID:def 1 ;
deffunc H₁( Element of n -tuples_on REAL) -> set = n . 1;
consider f being Function such that
A2: ( dom f = n -tuples_on REAL & ( for d being Element of n -tuples_on REAL holds f . d = H₁(d) ) ) from FUNCT_1:sch 4();
for y being object holds
( y in f .: (n -tuples_on REAL) iff y in REAL )

proof

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

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

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

end;

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

end;

hence not TOP-REAL n is finite by A1, TARSKI:2; :: thesis: verum