let S be RealNormSpace; :: thesis: for Y being Subset of S
for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y
let Y be Subset of S; :: thesis: for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds
f is_continuous_on Y
let f be PartFunc of S,S; :: thesis: ( Y c= dom f & f | Y = id Y implies f is_continuous_on Y )
assume that
A1: Y c= dom f and
A2: f | Y = id Y ; :: thesis: f is_continuous_on Y

now :: thesis: for x1, x2 being Point of S st x1 in Y & x2 in Y holds
||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||

let x1, x2 be Point of S; :: thesis: ( x1 in Y & x2 in Y implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| )
assume that
A3: x1 in Y and
A4: x2 in Y ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
x1 in (dom f) /\ Y by A1, A3, XBOOLE_0:def 4;
then A5: x1 in dom (f | Y) by RELAT_1:61;
(f | Y) . x1 = x1 by A2, A3, FUNCT_1:17;
then f . x1 = x1 by A5, FUNCT_1:47;
then A6: f /. x1 = x1 by A1, A3, PARTFUN1:def 6;
x2 in (dom f) /\ Y by A1, A4, XBOOLE_0:def 4;
then A7: x2 in dom (f | Y) by RELAT_1:61;
(f | Y) . x2 = x2 by A2, A4, FUNCT_1:17;
then f . x2 = x2 by A7, FUNCT_1:47;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by A1, A4, A6, PARTFUN1:def 6; :: thesis: verum

end;

then f is_Lipschitzian_on Y by A1;
hence f is_continuous_on Y by Th45; :: thesis: verum