let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st ex r being Point of S st rng f = {r} holds

f is continuous

let f be PartFunc of REAL, the carrier of S; :: thesis: ( ex r being Point of S st rng f = {r} implies f is continuous )

given r being Point of S such that A1: rng f = {r} ; :: thesis: f is continuous

hence f is continuous ; :: thesis: verum

f is continuous

let f be PartFunc of REAL, the carrier of S; :: thesis: ( ex r being Point of S st rng f = {r} implies f is continuous )

given r being Point of S such that A1: rng f = {r} ; :: thesis: f is continuous

now :: thesis: for x1, x2 being Real st x1 in dom f & x2 in dom f holds

||.((f /. x1) - (f /. x2)).|| <= 1 * |.(x1 - x2).|

then
f is Lipschitzian
;||.((f /. x1) - (f /. x2)).|| <= 1 * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * |.(x1 - x2).| )

assume A2: ( x1 in dom f & x2 in dom f ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * |.(x1 - x2).|

then f . x2 in rng f by FUNCT_1:def 3;

then f /. x2 in rng f by A2, PARTFUN1:def 6;

then A3: f /. x2 = r by A1, TARSKI:def 1;

f . x1 in rng f by A2, FUNCT_1:def 3;

then f /. x1 in rng f by A2, PARTFUN1:def 6;

then f /. x1 = r by A1, TARSKI:def 1;

then ||.((f /. x1) - (f /. x2)).|| = 0 by A3, NORMSP_1:6;

hence ||.((f /. x1) - (f /. x2)).|| <= 1 * |.(x1 - x2).| by COMPLEX1:46; :: thesis: verum

end;assume A2: ( x1 in dom f & x2 in dom f ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * |.(x1 - x2).|

then f . x2 in rng f by FUNCT_1:def 3;

then f /. x2 in rng f by A2, PARTFUN1:def 6;

then A3: f /. x2 = r by A1, TARSKI:def 1;

f . x1 in rng f by A2, FUNCT_1:def 3;

then f /. x1 in rng f by A2, PARTFUN1:def 6;

then f /. x1 = r by A1, TARSKI:def 1;

then ||.((f /. x1) - (f /. x2)).|| = 0 by A3, NORMSP_1:6;

hence ||.((f /. x1) - (f /. x2)).|| <= 1 * |.(x1 - x2).| by COMPLEX1:46; :: thesis: verum

hence f is continuous ; :: thesis: verum