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 )
assume A1: for p being Point of ((TOP-REAL n) | K0) holds f . p = (n NormF ) . p ; :: thesis: f is continuous
A2: dom f = the carrier of ((TOP-REAL n) | K0) by FUNCT_2:def 1;
A3: the carrier of ((TOP-REAL n) | K0) = K0 by PRE_TOPC:29;
the carrier of (TOP-REAL n) /\ K0 = K0 by XBOOLE_1:28;
then A4: dom f = (dom (n NormF )) /\ K0 by A2, A3, FUNCT_2:def 1;
A5: for x being set st x in dom f holds
f . x = (n NormF ) . x by A1;
reconsider g = n NormF as Function of (TOP-REAL n),R^1 ;
f = g | K0 by A4, A5, FUNCT_1:68;
hence f is continuous by Th19, TOPMETR:10; :: thesis: verum