let Z be RealNormSpace; :: thesis: for a, b, c, d being Real
for f being PartFunc of REAL, the carrier of Z st a <= c & c <= d & d <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
f | ['c,d'] is bounded
let a, b, c, d be Real; :: thesis: for f being PartFunc of REAL, the carrier of Z st a <= c & c <= d & d <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f holds
f | ['c,d'] is bounded
let f be PartFunc of REAL, the carrier of Z; :: thesis: ( a <= c & c <= d & d <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f implies f | ['c,d'] is bounded )
assume A1: ( a <= c & c <= d & d <= b & f | ['a,b'] is bounded & ['a,b'] c= dom f ) ; :: thesis: f | ['c,d'] is bounded
A2: ( c <= b & a <= d ) by A1, XXREAL_0:2;
then A4: ( c in ['a,b'] & d in ['a,b'] ) by A1, INTEGR19:1;
reconsider A = ['a,b'], B = ['c,d'] as non empty closed_interval Subset of REAL ;
( c = min (c,d) & d = max (c,d) ) by A1, XXREAL_0:def 9, XXREAL_0:def 10;
then A5: B c= A by A2, A1, XXREAL_0:2, A4, Lm2;
then B c= dom (f | A) by A1, RELAT_1:62;
hence f | ['c,d'] is bounded by A1, A5, Th1915a; :: thesis: verum