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;
A2: p . 1 = x by A1, FINSEQ_1:45;
p . 2 = y by A1, FINSEQ_1:45;
hence p = |[(p . 1),(p . 2),(p . 3)]| by A1, A2, FINSEQ_1:45; :: thesis: verum