let p be Element of (TOP-REAL 2); :: thesis: ( p /. 1 = p `1 & p /. 2 = p `2 )
reconsider r1 = p `1 , r2 = p `2 as Real ;
reconsider g = <*r1,r2*> as FinSequence of REAL by FINSEQ_2:15;
A2: p /. 2 = g /. 2 by EUCLID:57
.= p `2 by FINSEQ_4:26 ;
p /. 1 = g /. 1 by EUCLID:57
.= p `1 by FINSEQ_4:26 ;
hence ( p /. 1 = p `1 & p /. 2 = p `2 ) by A2; :: thesis: verum