let K be non empty Subset of (TOP-REAL 2); :: thesis: ( proj1 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj1 | K) . q = proj1 . q ) )
reconsider g2 = proj1 | K as Function of ((TOP-REAL 2) | K),R^1 by TOPMETR:17;
A1: the carrier of ((TOP-REAL 2) | K) = K by PRE_TOPC:8;
for q being Point of ((TOP-REAL 2) | K) holds g2 . q = proj1 . q

proof

let q be Point of ((TOP-REAL 2) | K); :: thesis: g2 . q = proj1 . q
( q in the carrier of ((TOP-REAL 2) | K) & dom proj1 = the carrier of (TOP-REAL 2) ) by FUNCT_2:def 1;
then q in (dom proj1) /\ K by A1, XBOOLE_0:def 4;
hence g2 . q = proj1 . q by FUNCT_1:48; :: thesis: verum

end;

hence ( proj1 | K is continuous Function of ((TOP-REAL 2) | K),R^1 & ( for q being Point of ((TOP-REAL 2) | K) holds (proj1 | K) . q = proj1 . q ) ) by JGRAPH_2:29; :: thesis: verum