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