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

proof

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

end;

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