let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T st ex r being Point of T st rng f = {r} holds
f is_continuous_on dom f
let f be PartFunc of S,T; :: thesis: ( ex r being Point of T st rng f = {r} implies f is_continuous_on dom f )
given r being Point of T such that A1: rng f = {r} ; :: 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 . x2 in rng f by A3, FUNCT_1:def 3;
then f /. x2 in rng f by A3, PARTFUN1:def 6;
then A4: 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. T).|| by A4, RLVECT_1:15
.= 0 by NORMSP_1:1 ;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by NORMSP_1:4; :: thesis: verum

end;

then f is_Lipschitzian_on dom f ;
hence f is_continuous_on dom f by Th45; :: thesis: verum