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