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 that
A1: X c= dom f and
A2: for x0 being Point of CNS st x0 in X holds
f /. x0 = ||.x0.|| ; :: thesis: f is_continuous_on X
X = (dom f) /\ X by A1, XBOOLE_1:28;
then A3: X = dom (f | X) by RELAT_1:61;
now :: thesis: for x0 being Point of CNS st x0 in dom (f | X) holds
(f | X) /. x0 = ||.x0.||
let x0 be Point of CNS; :: thesis: ( x0 in dom (f | X) implies (f | X) /. x0 = ||.x0.|| )
assume A4: x0 in dom (f | X) ; :: thesis: (f | X) /. x0 = ||.x0.||
hence (f | X) /. x0 = f /. x0 by PARTFUN2:15
.= ||.x0.|| by A2, A3, A4 ;
:: thesis: verum
end;
then f | X is_continuous_on X by A3, Th132;
hence f is_continuous_on X by Th54; :: thesis: verum