let p be Element of (TOP-REAL 2); :: thesis: ( Proj p,1 = proj1 . p & Proj p,2 = proj2 . p )
A1: proj1 . p = p `1 by PSCOMP_1:def 28
.= Proj p,1 by Th35 ;
proj2 . p = p `2 by PSCOMP_1:def 29
.= Proj p,2 by Th35 ;
hence ( Proj p,1 = proj1 . p & Proj p,2 = proj2 . p ) by A1; :: thesis: verum