let K1 be non empty Subset of (TOP-REAL 2); :: thesis: ( (2 NormF) | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1 & ( for q being Point of ((TOP-REAL 2) | K1) holds ((2 NormF) | K1) . q = (2 NormF) . q ) )
A1: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:8;
then reconsider g1 = (2 NormF) | K1 as Function of ((TOP-REAL 2) | K1),R^1 by FUNCT_2:32;
for q being Point of ((TOP-REAL 2) | K1) holds g1 . q = (2 NormF) . q

proof

let q be Point of ((TOP-REAL 2) | K1); :: thesis: g1 . q = (2 NormF) . q
q in the carrier of ((TOP-REAL 2) | K1) ;
then q in (dom (2 NormF)) /\ K1 by A1, Lm4, XBOOLE_0:def 4;
hence g1 . q = (2 NormF) . q by FUNCT_1:48; :: thesis: verum

end;

hence ( (2 NormF) | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1 & ( for q being Point of ((TOP-REAL 2) | K1) holds ((2 NormF) | K1) . q = (2 NormF) . q ) ) by Th13; :: thesis: verum