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
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).|
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;
0 + 0 < |.r.| + 1 by COMPLEX1:46, XREAL_1:8;
then f | X is Lipschitzian by A2, Th32;
hence f | X is continuous ; :: thesis: verum