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 A1: ( 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 ) ) ; :: thesis: ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a )
A2: ( dom f = A & dom g = A ) by FUNCT_2:def 1;
then A3: ( rng f is non empty Subset of REAL & rng g is non empty Subset of REAL ) by RELAT_1:65;
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
A4: ( x in dom f & b = f . x ) by PARTFUN1:26;
abs ((f . x) - (g . x)) <= a by A1;
then (f . x) - (g . x) <= a by ABSVALUE:12;
then A5: b <= a + (g . x) by A4, XREAL_1:22;
g . x in rng g by A2, FUNCT_1:12;
then g . x <= upper_bound (rng g) by A1, SEQ_4:def 4;
then a + (g . x) <= a + (upper_bound (rng g)) by XREAL_1:8;
hence b <= (upper_bound (rng g)) + a by A5, XXREAL_0:2; :: thesis: verum

end;

then A6: upper_bound (rng f) <= (upper_bound (rng g)) + a by A3, SEQ_4:62;
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
A7: ( x in dom g & b = g . x ) by PARTFUN1:26;
abs ((f . x) - (g . x)) <= a by A1;
then abs ((g . x) - (f . x)) <= a by COMPLEX1:146;
then (g . x) - (f . x) <= a by ABSVALUE:12;
then A8: b <= a + (f . x) by A7, XREAL_1:22;
f . x in rng f by A2, FUNCT_1:12;
then f . x <= upper_bound (rng f) by A1, SEQ_4:def 4;
then a + (f . x) <= a + (upper_bound (rng f)) by XREAL_1:8;
hence b <= (upper_bound (rng f)) + a by A8, XXREAL_0:2; :: thesis: verum

end;

then upper_bound (rng g) <= (upper_bound (rng f)) + a by A3, SEQ_4:62;
hence ( (upper_bound (rng f)) - (upper_bound (rng g)) <= a & (upper_bound (rng g)) - (upper_bound (rng f)) <= a ) by A6, XREAL_1:22; :: thesis: verum