let p be Element of (TOP-REAL 2); ( p /. 1 = p `1 & p /. 2 = p `2 )
reconsider r1 = p `1 , r2 = p `2 as Element of REAL by XREAL_0:def 1;
reconsider g = <*r1,r2*> as FinSequence of REAL by FINSEQ_2:13;
A1: p /. 2 =
g /. 2
by EUCLID:53
.=
p `2
by FINSEQ_4:17
;
p /. 1 =
g /. 1
by EUCLID:53
.=
p `1
by FINSEQ_4:17
;
hence
( p /. 1 = p `1 & p /. 2 = p `2 )
by A1; verum