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:103;
thus p = |[(p . 1),(p . 2),(p . 3)]| by A1; :: thesis: verum