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