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_below & rng g is bounded_below & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) holds
( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a )
let A be non empty set ; :: thesis: for f, g being Function of A,REAL st rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) holds
( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a )
let f, g be Function of A,REAL; :: thesis: ( rng f is bounded_below & rng g is bounded_below & ( for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ) implies ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) )
assume that
A1: rng f is bounded_below and
A2: rng g is bounded_below and
A3: for x being set st x in A holds
abs ((f . x) - (g . x)) <= a ; :: thesis: ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_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
(lower_bound (rng f)) - a <= b

proof

let b be real number ; :: thesis: ( b in rng g implies (lower_bound (rng f)) - a <= b )
assume b in rng g ; :: thesis: (lower_bound (rng f)) - a <= b
then consider x being Element of A such that
x in dom g and
A6: b = g . x by PARTFUN1:26;
f . x in rng f by A4, FUNCT_1:12;
then lower_bound (rng f) <= f . x by A1, SEQ_4:def 5;
then A7: (lower_bound (rng f)) - a <= (f . x) - a by XREAL_1:11;
abs ((f . x) - (g . x)) <= a by A3;
then (f . x) - (g . x) <= a by ABSVALUE:12;
then (f . x) - a <= b by A6, XREAL_1:14;
hence (lower_bound (rng f)) - a <= b 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:65;
then A9: (lower_bound (rng f)) - a <= lower_bound (rng g) by A5, SEQ_4:60;
A10: for b being real number st b in rng f holds
(lower_bound (rng g)) - a <= b

proof

let b be real number ; :: thesis: ( b in rng f implies (lower_bound (rng g)) - a <= b )
assume b in rng f ; :: thesis: (lower_bound (rng g)) - a <= b
then consider x being Element of A such that
x in dom f and
A11: b = f . x by PARTFUN1:26;
abs ((f . x) - (g . x)) <= a by A3;
then abs ((g . x) - (f . x)) <= a by COMPLEX1:146;
then (g . x) - (f . x) <= a by ABSVALUE:12;
then A12: (g . x) - a <= b by A11, XREAL_1:14;
g . x in rng g by A8, FUNCT_1:12;
then lower_bound (rng g) <= g . x by A2, SEQ_4:def 5;
then (lower_bound (rng g)) - a <= (g . x) - a by XREAL_1:11;
hence (lower_bound (rng g)) - a <= b by A12, XXREAL_0:2; :: thesis: verum

end;

rng f is non empty Subset of REAL by A4, RELAT_1:65;
then (lower_bound (rng g)) - a <= lower_bound (rng f) by A10, SEQ_4:60;
hence ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) by A9, XREAL_1:14; :: thesis: verum