let f be Function of (TOP-REAL 2),R^1 ; :: thesis: ( f = proj1 implies f is continuous )
assume A1: f = proj1 ; :: thesis: f is continuous
A2: 1 in Seg 2 by FINSEQ_1:3;
for p being Element of (TOP-REAL 2) holds f . p = Proj p,1 by A1, JORDAN2B:36;
hence f is continuous by A2, JORDAN2B:22; :: thesis: verum