let f be Function of (TOP-REAL 2),R^1; :: thesis: ( f = proj2 implies f is continuous )
assume f = proj2 ; :: thesis: f is continuous
then ( 2 in Seg 2 & ( for p being Element of (TOP-REAL 2) holds f . p = p /. 2 ) ) by FINSEQ_1:1, JORDAN2B:30;
hence f is continuous by JORDAN2B:18; :: thesis: verum