let r be Real; 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 ; 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; ( f - g,X is_absolutely_bounded_by r implies g - f,X is_absolutely_bounded_by r )
assume A1:
f - g,X is_absolutely_bounded_by r
; g - f,X is_absolutely_bounded_by r
let x be set ; TIETZE:def 1 ( x in X /\ (dom (g - f)) implies |.((g - f) . x).| <= r )
assume A2:
x in X /\ (dom (g - f))
; |.((g - f) . x).| <= r
then A3:
x in dom (g - f)
by XBOOLE_0:def 4;
A4: dom (f - g) =
(dom f) /\ (dom g)
by VALUED_1:12
.=
dom (g - f)
by VALUED_1:12
;
then
|.((f - g) . x).| <= r
by A1, A2;
then
|.((f . x) - (g . x)).| <= r
by A4, A3, VALUED_1:13;
then
|.(- ((f . x) - (g . x))).| <= r
by COMPLEX1:52;
then
|.((g . x) - (f . x)).| <= r
;
hence
|.((g - f) . x).| <= r
by A3, VALUED_1:13; verum