let K1 be non empty Subset of (TOP-REAL 2); :: thesis: proj2 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1

reconsider g2 = proj2 | K1 as Function of ((TOP-REAL 2) | K1),R^1 by TOPMETR:17;

for q being Point of ((TOP-REAL 2) | K1) holds g2 . q = proj2 . q by Lm4;

hence proj2 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1 by JGRAPH_2:30; :: thesis: verum

reconsider g2 = proj2 | K1 as Function of ((TOP-REAL 2) | K1),R^1 by TOPMETR:17;

for q being Point of ((TOP-REAL 2) | K1) holds g2 . q = proj2 . q by Lm4;

hence proj2 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1 by JGRAPH_2:30; :: thesis: verum