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