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