let p be Point of (TOP-REAL 3); :: thesis: p = <*(p `1),(p `2),(p `3)*>
reconsider f = p as FinSequence ;
consider x, y, z being Real such that
A1: p = <*x,y,z*> by Th1;
<*x,y,z*> = <*(f . 1),y,z*> by A1, FINSEQ_1:45
.= <*(f . 1),(f . 2),z*> by A1, FINSEQ_1:45
.= <*(p `1),(p `2),(p `3)*> by A1, FINSEQ_1:45 ;
hence p = <*(p `1),(p `2),(p `3)*> by A1; :: thesis: verum