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 A1: for x0 being real number st x0 in X holds
f . x0 = (r * x0) + p ; :: thesis: f | X is continuous

A2: 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 that
A3: x1 in dom (f | X) and
A4: x2 in dom (f | X) ; :: thesis: abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2))
x2 in X by A4, RELAT_1:86;
then A5: f . x2 = (r * x2) + p by A1;
A6: 0 <= abs (x1 - x2) by COMPLEX1:132;
x1 in X by A3, RELAT_1:86;
then f . x1 = (r * x1) + p by A1;
then abs ((f . x1) - (f . x2)) = abs (r * (x1 - x2)) by A5
.= (abs r) * (abs (x1 - x2)) by COMPLEX1:151 ;
then (abs ((f . x1) - (f . x2))) + 0 <= ((abs r) * (abs (x1 - x2))) + (1 * (abs (x1 - x2))) by A6, XREAL_1:9;
hence abs ((f . x1) - (f . x2)) <= ((abs r) + 1) * (abs (x1 - x2)) ; :: thesis: verum

end;

0 + 0 < (abs r) + 1 by COMPLEX1:132, XREAL_1:10;
then f | X is Lipschitzian by A2, Th33;
hence f | X is continuous ; :: thesis: verum