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
reconsider f = f as Function of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #),R^1 ;
(TOP-REAL 2) | ([#] (TOP-REAL 2)) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by TSEP_1:93;
then f is continuous by A1, JGRAPH_2:29;
hence f is continuous by PRE_TOPC:32; :: thesis: verum