let a be Real; :: 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
|.((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
|.((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
|.((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
|.((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 st b in rng g holds
(lower_bound (rng f)) - a <= b

proof

let b be Real; :: 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:3;
f . x in rng f by A4, FUNCT_1:3;
then lower_bound (rng f) <= f . x by A1, SEQ_4:def 2;
then A7: (lower_bound (rng f)) - a <= (f . x) - a by XREAL_1:9;
|.((f . x) - (g . x)).| <= a by A3;
then (f . x) - (g . x) <= a by ABSVALUE:5;
then (f . x) - a <= b by A6, XREAL_1:12;
hence (lower_bound (rng f)) - a <= b by A7, XXREAL_0:2; :: thesis: verum

end;

A8: dom g = A by FUNCT_2:def 1;
A9: (lower_bound (rng f)) - a <= lower_bound (rng g) by A5, SEQ_4:43;
A10: for b being Real st b in rng f holds
(lower_bound (rng g)) - a <= b

proof

let b be Real; :: 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:3;
|.((f . x) - (g . x)).| <= a by A3;
then |.((g . x) - (f . x)).| <= a by COMPLEX1:60;
then (g . x) - (f . x) <= a by ABSVALUE:5;
then A12: (g . x) - a <= b by A11, XREAL_1:12;
g . x in rng g by A8, FUNCT_1:3;
then lower_bound (rng g) <= g . x by A2, SEQ_4:def 2;
then (lower_bound (rng g)) - a <= (g . x) - a by XREAL_1:9;
hence (lower_bound (rng g)) - a <= b by A12, XXREAL_0:2; :: thesis: verum

end;

(lower_bound (rng g)) - a <= lower_bound (rng f) by A10, SEQ_4:43;
hence ( (lower_bound (rng f)) - (lower_bound (rng g)) <= a & (lower_bound (rng g)) - (lower_bound (rng f)) <= a ) by A9, XREAL_1:12; :: thesis: verum