let p be Point of (TOP-REAL 2); :: thesis: p = |[(proj1 . p),(proj2 . p)]|
A1: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
p `1 = proj1 . p by PSCOMP_1:def 28;
hence p = |[(proj1 . p),(proj2 . p)]| by A1, PSCOMP_1:def 29; :: thesis: verum