let p be Point of (TOP-REAL 2); :: thesis: p = |[(p `1 ),(p `2 )]|
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by Def8;
then consider x, y being Real such that
A1: p = <*x,y*> by FINSEQ_2:120;
( p `1 = x & p `2 = y ) by A1, FINSEQ_1:61;
hence p = |[(p `1 ),(p `2 )]| by A1; :: thesis: verum