let a be real number ; :: thesis: for A being non empty set
for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) holds
( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a )
let A be non empty set ; :: thesis: for f, g being Function of A,REAL st rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) holds
( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a )
let f, g be Function of A,REAL; :: thesis: ( rng f is bounded_above & rng g is bounded_above & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) implies ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) )
assume that
A1: rng f is bounded_above and
A2: rng g is bounded_above and
A3: for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ; :: thesis: ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a )
A4: dom f = A by FUNCT_2:def 1;
A5: for b being real number st b in rng g holds
b <= (upper_bound (rng f)) + a

proof

let b be real number ; :: thesis: ( b in rng g implies b <= (upper_bound (rng f)) + a )
assume b in rng g ; :: thesis: b <= (upper_bound (rng f)) + a
then consider x being Element of A such that
x in dom g and
A6: b = g . x by PARTFUN1:3;
abs ((f . x) - (g . x)) <= a by A3;
then abs ((g . x) - (f . x)) <= a by COMPLEX1:60;
then (g . x) - (f . x) <= a by ABSVALUE:5;
then A7: b <= a + (f . x) by A6, XREAL_1:20;
f . x in rng f by A4, FUNCT_1:3;
then f . x <= upper_bound (rng f) by A1, SEQ_4:def 1;
then a + (f . x) <= a + (upper_bound (rng f)) by XREAL_1:6;
hence b <= (upper_bound (rng f)) + a by A7, XXREAL_0:2; :: thesis: verum

end;

A8: dom g = A by FUNCT_2:def 1;
then rng g is non empty Subset of REAL by RELAT_1:42;
then A9: upper_bound (rng g) <= (upper_bound (rng f)) + a by A5, SEQ_4:45;
A10: for b being real number st b in rng f holds
b <= (upper_bound (rng g)) + a

proof

let b be real number ; :: thesis: ( b in rng f implies b <= (upper_bound (rng g)) + a )
assume b in rng f ; :: thesis: b <= (upper_bound (rng g)) + a
then consider x being Element of A such that
x in dom f and
A11: b = f . x by PARTFUN1:3;
g . x in rng g by A8, FUNCT_1:3;
then g . x <= upper_bound (rng g) by A2, SEQ_4:def 1;
then A12: a + (g . x) <= a + (upper_bound (rng g)) by XREAL_1:6;
abs ((f . x) - (g . x)) <= a by A3;
then (f . x) - (g . x) <= a by ABSVALUE:5;
then b <= a + (g . x) by A11, XREAL_1:20;
hence b <= (upper_bound (rng g)) + a by A12, XXREAL_0:2; :: thesis: verum

end;

rng f is non empty Subset of REAL by A4, RELAT_1:42;
then upper_bound (rng f) <= (upper_bound (rng g)) + a by A10, SEQ_4:45;
hence ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) by A9, XREAL_1:20; :: thesis: verum