let f be Function of (TOP-REAL 2),R^1 ; :: thesis: ( ( for p being Point of (TOP-REAL 2) holds f . p = proj1 . p ) implies f is continuous )
assume A1: for p being Point of (TOP-REAL 2) holds f . p = proj1 . p ; :: thesis: f is continuous
(TOP-REAL 2) | ([#] (TOP-REAL 2)) = TOP-REAL 2 by TSEP_1:3;
hence f is continuous by A1, JGRAPH_2:39; :: thesis: verum