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 A1: ( 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 ) ) ; :: thesis: ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_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
(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
A4: ( x in dom f & b = f . 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 A5: (g . x) - a <= b by A4, XREAL_1:14;
g . x in rng g by A2, FUNCT_1:12;
then lower_bound (rng g) <= g . x by A1, 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 A5, XXREAL_0:2; :: thesis: verum

end;

then A6: (lower_bound (rng g)) - a <= lower_bound (rng f) by A3, SEQ_4:60;
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
A7: ( x in dom g & b = g . x ) by PARTFUN1:26;
abs ((f . x) - (g . x)) <= a by A1;
then (f . x) - (g . x) <= a by ABSVALUE:12;
then A8: (f . x) - a <= b by A7, XREAL_1:14;
f . x in rng f by A2, FUNCT_1:12;
then lower_bound (rng f) <= f . x by A1, SEQ_4:def 5;
then (lower_bound (rng f)) - a <= (f . x) - a by XREAL_1:11;
hence (lower_bound (rng f)) - a <= b by A8, XXREAL_0:2; :: thesis: verum

end;

then (lower_bound (rng f)) - a <= lower_bound (rng g) by A3, SEQ_4:60;
hence ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) by A6, XREAL_1:14; :: thesis: verum