let r be real number ; :: thesis: for X being set
for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds
g - f,X is_absolutely_bounded_by r
let X be set ; :: thesis: for f, g being real-valued Function st f - g,X is_absolutely_bounded_by r holds
g - f,X is_absolutely_bounded_by r
let f, g be real-valued Function; :: thesis: ( f - g,X is_absolutely_bounded_by r implies g - f,X is_absolutely_bounded_by r )
A1: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12
.= dom (g - f) by VALUED_1:12 ;
assume A2: f - g,X is_absolutely_bounded_by r ; :: thesis: g - f,X is_absolutely_bounded_by r
let x be set ; :: according to TIETZE:def 1 :: thesis: ( x in X /\ (dom (g - f)) implies abs ((g - f) . x) <= r )
assume A3: x in X /\ (dom (g - f)) ; :: thesis: abs ((g - f) . x) <= r
then A4: x in dom (g - f) by XBOOLE_0:def 4;
abs ((f - g) . x) <= r by A1, A2, A3, Def1;
then abs ((f . x) - (g . x)) <= r by A1, A4, VALUED_1:13;
then abs (- ((f . x) - (g . x))) <= r by COMPLEX1:138;
then abs ((g . x) - (f . x)) <= r ;
hence abs ((g - f) . x) <= r by A4, VALUED_1:13; :: thesis: verum