let f be Function of (TOP-REAL 2),R^1 ; :: thesis: ( ( for p being Point of (TOP-REAL 2) holds f . p = proj2 . p ) implies f is continuous )
assume A1: for p being Point of (TOP-REAL 2) holds f . p = proj2 . 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:100;
then f is continuous by A1, JGRAPH_2:40;
hence f is continuous by PRE_TOPC:62; :: thesis: verum