let p be Element of REAL 3; :: thesis: p = <*(p . 1),(p . 2),(p . 3)*>
consider x, y, z being Element of REAL such that
A1: p = <*x,y,z*> by FINSEQ_2:123;
<*x,y,z*> = <*(p . 1),y,z*> by A1, FINSEQ_1:62
.= <*(p . 1),(p . 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