let X be set ; :: thesis: for r, p being real number
for f being PartFunc of REAL ,REAL st ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) holds
f | X is continuous
let r, p be real number ; :: thesis: for f being PartFunc of REAL ,REAL st ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) holds
f | X is continuous
let f be PartFunc of REAL ,REAL ; :: thesis: ( ( for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ) implies f | X is continuous )
assume A2: for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ; :: thesis: f | X is continuous
A3: 0 + 0 < (abs r) + 1 by COMPLEX1:132, XREAL_1:10;

now

let x1, x2 be real number ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2)) )
assume ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2))
then ( x1 in X & x2 in X ) by RELAT_1:86;
then ( f . x1 = (r * x1) + p & f . x2 = (r * x2) + p ) by A2;
then A4: abs ((f . x1) - (f . x2)) = abs (r * (x1 - x2))
.= (abs r) * (abs (x1 - x2)) by COMPLEX1:151 ;
0 <= abs (x1 - x2) by COMPLEX1:132;
then (abs ((f . x1) - (f . x2))) + 0 <= ((abs r) * (abs (x1 - x2))) + (1 * (abs (x1 - x2))) by A4, XREAL_1:9;
hence abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2)) ; :: thesis: verum

end;

then f | X is Lipschitzian by A3, Def3;
hence f | X is continuous ; :: thesis: verum