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