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 p is Tuple of 2, REAL by FINSEQ_2:131;
then consider x, y being Element of REAL such that
A1: p = <*x,y*> by FINSEQ_2:100;
p `1 = x by A1, FINSEQ_1:44;
hence p = |[(p `1),(p `2)]| by A1, FINSEQ_1:44; :: thesis: verum