let X be set ; :: thesis: for r, p being Real

for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in X holds

f . x0 = (r * x0) + p ) holds

f | X is continuous

let r, p be Real; :: thesis: for f being PartFunc of REAL,REAL st ( for x0 being Real 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 st x0 in X holds

f . x0 = (r * x0) + p ) implies f | X is continuous )

assume A1: for x0 being Real st x0 in X holds

f . x0 = (r * x0) + p ; :: thesis: f | X is continuous

then f | X is Lipschitzian by A2, Th32;

hence f | X is continuous ; :: thesis: verum

for f being PartFunc of REAL,REAL st ( for x0 being Real st x0 in X holds

f . x0 = (r * x0) + p ) holds

f | X is continuous

let r, p be Real; :: thesis: for f being PartFunc of REAL,REAL st ( for x0 being Real 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 st x0 in X holds

f . x0 = (r * x0) + p ) implies f | X is continuous )

assume A1: for x0 being Real st x0 in X holds

f . x0 = (r * x0) + p ; :: thesis: f | X is continuous

A2: now :: thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds

|.((f . x1) - (f . x2)).| <= (|.r.| + 1) * |.(x1 - x2).|

0 + 0 < |.r.| + 1
by COMPLEX1:46, XREAL_1:8;|.((f . x1) - (f . x2)).| <= (|.r.| + 1) * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.((f . x1) - (f . x2)).| <= (|.r.| + 1) * |.(x1 - x2).| )

assume that

A3: x1 in dom (f | X) and

A4: x2 in dom (f | X) ; :: thesis: |.((f . x1) - (f . x2)).| <= (|.r.| + 1) * |.(x1 - x2).|

x2 in X by A4;

then A5: f . x2 = (r * x2) + p by A1;

A6: 0 <= |.(x1 - x2).| by COMPLEX1:46;

x1 in X by A3;

then f . x1 = (r * x1) + p by A1;

then |.((f . x1) - (f . x2)).| = |.(r * (x1 - x2)).| by A5

.= |.r.| * |.(x1 - x2).| by COMPLEX1:65 ;

then |.((f . x1) - (f . x2)).| + 0 <= (|.r.| * |.(x1 - x2).|) + (1 * |.(x1 - x2).|) by A6, XREAL_1:7;

hence |.((f . x1) - (f . x2)).| <= (|.r.| + 1) * |.(x1 - x2).| ; :: thesis: verum

end;assume that

A3: x1 in dom (f | X) and

A4: x2 in dom (f | X) ; :: thesis: |.((f . x1) - (f . x2)).| <= (|.r.| + 1) * |.(x1 - x2).|

x2 in X by A4;

then A5: f . x2 = (r * x2) + p by A1;

A6: 0 <= |.(x1 - x2).| by COMPLEX1:46;

x1 in X by A3;

then f . x1 = (r * x1) + p by A1;

then |.((f . x1) - (f . x2)).| = |.(r * (x1 - x2)).| by A5

.= |.r.| * |.(x1 - x2).| by COMPLEX1:65 ;

then |.((f . x1) - (f . x2)).| + 0 <= (|.r.| * |.(x1 - x2).|) + (1 * |.(x1 - x2).|) by A6, XREAL_1:7;

hence |.((f . x1) - (f . x2)).| <= (|.r.| + 1) * |.(x1 - x2).| ; :: thesis: verum

then f | X is Lipschitzian by A2, Th32;

hence f | X is continuous ; :: thesis: verum