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 Element of REAL such that
A1: p = <*x,y,z*> by Th1;
<*x,y,z*> = <*(f . 1),y,z*> by A1, FINSEQ_1:62
.= <*(f . 1),(f . 2),z*> by A1, FINSEQ_1:62
.= <*(p `1 ),(p `2 ),(p `3 )*> by A1, FINSEQ_1:62 ;
hence p = <*(p `1 ),(p `2 ),(p `3 )*> by A1; :: thesis: verum