let X be set ; :: thesis:
let S be RealNormSpace; :: thesis:
let f be PartFunc of S,S; :: thesis:
let r be Real; :: thesis:
let p be Point of S; :: thesis:
assume that
A1: X c= dom f and
A2: for x0 being Point of S st x0 in X holds
f /. x0 = (r * x0) + p ; :: thesis:

now :: thesis:

0 + 0 < |.r.| + 1 by COMPLEX1:46, XREAL_1:8;
hence 0 < |.r.| + 1 ; :: thesis:
let x1, x2 be Point of S; :: thesis:
assume ( x1 in X & x2 in X ) ; :: thesis:
then ( f /. x1 = (r * x1) + p & f /. x2 = (r * x2) + p ) by A2;
then A3: ||.((f /. x1) - (f /. x2)).|| = ||.((r * x1) + (p - (p + (r * x2)))).|| by RLVECT_1:def 3
.= ||.((r * x1) + ((p - p) - (r * x2))).|| by RLVECT_1:27
.= ||.((r * x1) + ((0. S) - (r * x2))).|| by RLVECT_1:15
.= ||.((r * x1) - (r * x2)).||
.= ||.(r * (x1 - x2)).|| by RLVECT_1:34
.= |.r.| * ||.(x1 - x2).|| by NORMSP_1:def 1 ;
0 <= ||.(x1 - x2).|| by NORMSP_1:4;
then ||.((f /. x1) - (f /. x2)).|| + 0 <= (|.r.| * ||.(x1 - x2).||) + (1 * ||.(x1 - x2).||) by A3, XREAL_1:7;
hence ||.((f /. x1) - (f /. x2)).|| <= (|.r.| + 1) * ||.(x1 - x2).|| ; :: thesis:

end;

then f is_Lipschitzian_on X by A1;
hence f is_continuous_on X by Th45; :: thesis: