let p be Element of (TOP-REAL 2); :: thesis: ( p /. 1 = proj1 . p & p /. 2 = proj2 . p )
A1: proj2 . p = p `2 by PSCOMP_1:def 6
.= p /. 2 by Th29 ;
proj1 . p = p `1 by PSCOMP_1:def 5
.= p /. 1 by Th29 ;
hence ( p /. 1 = proj1 . p & p /. 2 = proj2 . p ) by A1; :: thesis: verum