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

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

hence f is continuous ; :: thesis: verum

given r being Real 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 that

A2: x1 in dom f and

A3: x2 in dom f ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

f . x2 in rng f by A3, FUNCT_1:def 3;

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

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

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

then |.((f . x1) - (f . x2)).| = 0 by A4, ABSVALUE:2;

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

end;assume that

A2: x1 in dom f and

A3: x2 in dom f ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

f . x2 in rng f by A3, FUNCT_1:def 3;

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

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

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

then |.((f . x1) - (f . x2)).| = 0 by A4, ABSVALUE:2;

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

hence f is continuous ; :: thesis: verum