let CNS be ComplexNormSpace; :: thesis: for f being PartFunc of CNS,CNS
for Y being Subset of CNS st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y
let f be PartFunc of CNS,CNS; :: thesis: for Y being Subset of CNS st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y
let Y be Subset of CNS; :: thesis: ( Y c= dom f & f | Y = id Y implies f is_continuous_on Y )
assume A1: ( Y c= dom f & f | Y = id Y ) ; :: thesis: f is_continuous_on Y

now

let x1, x2 be Point of CNS; :: thesis: ( x1 in Y & x2 in Y implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| )
assume A2: ( x1 in Y & x2 in Y ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
then ( x1 in (dom f) /\ Y & x2 in (dom f) /\ Y ) by A1, XBOOLE_0:def 4;
then A3: ( x1 in dom (f | Y) & x2 in dom (f | Y) ) by RELAT_1:90;
( (f | Y) . x1 = x1 & (f | Y) . x2 = x2 ) by A1, A2, FUNCT_1:34;
then ( f . x1 = x1 & f . x2 = x2 ) by A3, FUNCT_1:70;
then ( f /. x1 = x1 & f /. x2 = x2 ) by A1, A2, PARTFUN1:def 8;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| ; :: thesis: verum

end;

then f is_Lipschitzian_on Y by A1, Def27;
hence f is_continuous_on Y by Th137; :: thesis: verum