let a be Real; :: thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds
|.((f . x) - (f . y)).| <= a ) holds
(upper_bound (rng f)) - (lower_bound (rng f)) <= a
let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st ( for x, y being Real st x in A & y in A holds
|.((f . x) - (f . y)).| <= a ) holds
(upper_bound (rng f)) - (lower_bound (rng f)) <= a
let f be Function of A,REAL; :: thesis: ( ( for x, y being Real st x in A & y in A holds
|.((f . x) - (f . y)).| <= a ) implies (upper_bound (rng f)) - (lower_bound (rng f)) <= a )
assume A1: for x, y being Real st x in A & y in A holds
|.((f . x) - (f . y)).| <= a ; :: thesis: (upper_bound (rng f)) - (lower_bound (rng f)) <= a
A2: for y being Real st y in A holds
(upper_bound (rng f)) - a <= f . y

proof

let y be Real; :: thesis: ( y in A implies (upper_bound (rng f)) - a <= f . y )
assume A3: y in A ; :: thesis: (upper_bound (rng f)) - a <= f . y
for b being Real st b in rng f holds
b <= a + (f . y)

proof

let b be Real; :: thesis: ( b in rng f implies b <= a + (f . y) )
assume b in rng f ; :: thesis: b <= a + (f . y)
then consider x being Element of A such that
x in dom f and
A4: b = f . x by PARTFUN1:3;
|.((f . x) - (f . y)).| <= a by A1, A3;
then (f . x) - (f . y) <= a by ABSVALUE:5;
hence b <= a + (f . y) by A4, XREAL_1:20; :: thesis: verum

end;

then upper_bound (rng f) <= a + (f . y) by SEQ_4:45;
hence (upper_bound (rng f)) - a <= f . y by XREAL_1:20; :: thesis: verum

end;

for b being Real st b in rng f holds
(upper_bound (rng f)) - a <= b

proof

let b be Real; :: thesis: ( b in rng f implies (upper_bound (rng f)) - a <= b )
assume b in rng f ; :: thesis: (upper_bound (rng f)) - a <= b
then ex x being Element of A st
( x in dom f & b = f . x ) by PARTFUN1:3;
hence (upper_bound (rng f)) - a <= b by A2; :: thesis: verum

end;

then (upper_bound (rng f)) - a <= lower_bound (rng f) by SEQ_4:43;
then upper_bound (rng f) <= a + (lower_bound (rng f)) by XREAL_1:20;
hence (upper_bound (rng f)) - (lower_bound (rng f)) <= a by XREAL_1:20; :: thesis: verum