reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
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 = proj1 . 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 = proj1 . 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;
A2: g is continuous by JORDAN5A:27;
assume for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj1 . p ; :: thesis: f is continuous
then A3: for x being object st x in dom f holds
f . x = proj1 . x ;
the carrier of ((TOP-REAL 2) | K0) = [#] ((TOP-REAL 2) | K0)
.= K0 by PRE_TOPC:def 5 ;
then f = g | K0 by A1, A3, Th6, FUNCT_1:46;
hence f is continuous by A2, TOPMETR:7; :: thesis: verum