let K1 be non empty Subset of (TOP-REAL 2); :: thesis: proj1 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1
reconsider g2 = proj1 | 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 = proj1 . q by Lm6;
hence proj1 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1 by JGRAPH_2:29; :: thesis: verum