let K0 be Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | K0),R^1 st ( for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj2 . p ) holds
f is continuous
let f be Function of ((TOP-REAL 2) | K0),R^1; :: thesis: ( ( for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj2 . p ) implies f is continuous )
A1: ( dom f = the carrier of ((TOP-REAL 2) | K0) & the carrier of (TOP-REAL 2) /\ K0 = K0 ) by FUNCT_2:def 1, XBOOLE_1:28;
assume for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj2 . p ; :: thesis: f is continuous
then A2: for x being object st x in dom f holds
f . x = proj2 . x ;
the carrier of ((TOP-REAL 2) | K0) = [#] ((TOP-REAL 2) | K0)
.= K0 by PRE_TOPC:def 5 ;
then f = proj2 | K0 by A1, A2, Th7, FUNCT_1:46;
hence f is continuous by JORDAN5A:27; :: thesis: verum