let S be RealNormSpace; :: thesis: for f being PartFunc of S,S st ( for x0 being Point of S st x0 in dom f holds
f /. x0 = x0 ) holds
f is_continuous_on dom f
let f be PartFunc of S,S; :: thesis: ( ( for x0 being Point of S st x0 in dom f holds
f /. x0 = x0 ) implies f is_continuous_on dom f )
assume A1: for x0 being Point of S st x0 in dom f holds
f /. x0 = x0 ; :: thesis: f is_continuous_on dom f
now :: thesis: for x1, x2 being Point of S st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
let x1, x2 be Point of S; :: thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| )
assume that
A2: x1 in dom f and
A3: x2 in dom f ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
f /. x1 = x1 by A1, A2;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by A1, A3; :: thesis: verum
end;
then f is_Lipschitzian_on dom f ;
hence f is_continuous_on dom f by Th45; :: thesis: verum