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:29;
then reconsider g1 = (2 NormF ) | K1 as Function of ((TOP-REAL 2) | K1),R^1 by FUNCT_2:38;
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:71; :: 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 Th20; :: thesis: verum