let x be Point of (REAL-NS 1); :: thesis: ex z being Real st x = <*z*>
x is Element of REAL 1 by REAL_NS1:def 4;
then ex z being Element of REAL st x = <*z*> by FINSEQ_2:97;
hence ex z being Real st x = <*z*> ; :: thesis: verum