let p be Element of (TOP-REAL 1); :: thesis: ex r being Real st p = <*r*>
1 -tuples_on REAL = REAL 1 ;
then reconsider p9 = p as Element of 1 -tuples_on REAL by EUCLID:22;
ex r being Element of REAL st p9 = <*r*> by FINSEQ_2:97;
hence ex r being Real st p = <*r*> ; :: thesis: verum