let r be Real; :: 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 )
assume A1: 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 |.((g - f) . x).| <= r )
assume A2: x in X /\ (dom (g - f)) ; :: thesis: |.((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; :: thesis: verum