reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
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 TOPREAL6:83;
assume for p being Point of ((TOP-REAL 2) | K0) holds f . p = proj1 . p ; :: thesis: f is continuous
then A3: for x being set 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 10 ;
then f = g | K0 by A1, A3, Th14, FUNCT_1:68;
hence f is continuous by A2, TOPMETR:10; :: thesis: verum