let p be Point of (TOP-REAL 3); :: thesis: p = |[(p `1 ),(p `2 ),(p `3 )]|
consider x, y, z being Real such that
A1: p = <*x,y,z*> by Th1;
A2: p `1 = x by A1, FINSEQ_1:62;
p `2 = y by A1, FINSEQ_1:62;
hence p = |[(p `1 ),(p `2 ),(p `3 )]| by A1, A2, FINSEQ_1:62; :: thesis: verum