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

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