let CNS be ComplexNormSpace; :: thesis: for X being set
for f being PartFunc of the carrier of CNS,REAL st X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = ||.x0.|| ) holds
f is_continuous_on X
let X be set ; :: thesis: for f being PartFunc of the carrier of CNS,REAL st X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = ||.x0.|| ) holds
f is_continuous_on X
let f be PartFunc of the carrier of CNS,REAL ; :: thesis: ( X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = ||.x0.|| ) implies f is_continuous_on X )
assume A1: ( X c= dom f & ( for x0 being Point of CNS st x0 in X holds
f /. x0 = ||.x0.|| ) ) ; :: thesis: f is_continuous_on X
then X = (dom f) /\ X by XBOOLE_1:28;
then A2: X = dom (f | X) by RELAT_1:90;

now

let x0 be Point of CNS; :: thesis: ( x0 in dom (f | X) implies (f | X) /. x0 = ||.x0.|| )
assume A3: x0 in dom (f | X) ; :: thesis: (f | X) /. x0 = ||.x0.||
hence (f | X) /. x0 = f /. x0 by PARTFUN2:32
.= ||.x0.|| by A1, A2, A3 ;
:: thesis: verum

end;

then f | X is_continuous_on X by A2, Th153;
hence f is_continuous_on X by Th75; :: thesis: verum