let n be Element of NAT ; :: thesis: for K0 being Subset of (TOP-REAL n)
for f being Function of ((TOP-REAL n) | K0),R^1 st ( for p being Point of ((TOP-REAL n) | K0) holds f . p = (n NormF) . p ) holds
f is continuous
let K0 be Subset of (TOP-REAL n); :: thesis: for f being Function of ((TOP-REAL n) | K0),R^1 st ( for p being Point of ((TOP-REAL n) | K0) holds f . p = (n NormF) . p ) holds
f is continuous
let f be Function of ((TOP-REAL n) | K0),R^1; :: thesis: ( ( for p being Point of ((TOP-REAL n) | K0) holds f . p = (n NormF) . p ) implies f is continuous )
A1: the carrier of (TOP-REAL n) /\ K0 = K0 by XBOOLE_1:28;
reconsider g = n NormF as Function of (TOP-REAL n),R^1 ;
assume for p being Point of ((TOP-REAL n) | K0) holds f . p = (n NormF) . p ; :: thesis: f is continuous
then A2: for x being object st x in dom f holds
f . x = (n NormF) . x ;
( dom f = the carrier of ((TOP-REAL n) | K0) & the carrier of ((TOP-REAL n) | K0) = K0 ) by FUNCT_2:def 1, PRE_TOPC:8;
then dom f = (dom (n NormF)) /\ K0 by A1, FUNCT_2:def 1;
then f = g | K0 by A2, FUNCT_1:46;
hence f is continuous by TOPMETR:7; :: thesis: verum