let f be PartFunc of REAL,REAL; :: thesis: ( ex r being real number st rng f = {r} implies f is continuous )
given r being real number such that A1: rng f = {r} ; :: thesis: f is continuous

now

let x1, x2 be real number ; :: thesis: ( x1 in dom f & x2 in dom f implies abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) )
assume that
A2: x1 in dom f and
A3: x2 in dom f ; :: thesis: abs ((f . x1) - (f . x2)) <= 1 * (abs (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 abs ((f . x1) - (f . x2)) = 0 by A4, ABSVALUE:2;
hence abs ((f . x1) - (f . x2)) <= 1 * (abs (x1 - x2)) by COMPLEX1:46; :: thesis: verum

end;

then f is Lipschitzian by Def3;
hence f is continuous ; :: thesis: verum