let p, g be Real; :: thesis: for f being PartFunc of REAL ,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds
0 < diff f,x0 or for x0 being Real st x0 in ].p,g.[ holds
diff f,x0 < 0 ) holds
rng (f | ].p,g.[) is open
let f be PartFunc of REAL ,REAL ; :: thesis: ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds
0 < diff f,x0 or for x0 being Real st x0 in ].p,g.[ holds
diff f,x0 < 0 ) implies rng (f | ].p,g.[) is open )
assume Z: ].p,g.[ c= dom f ; :: thesis: ( not f is_differentiable_on ].p,g.[ or ( ex x0 being Real st
( x0 in ].p,g.[ & not 0 < diff f,x0 ) & ex x0 being Real st
( x0 in ].p,g.[ & not diff f,x0 < 0 ) ) or rng (f | ].p,g.[) is open )
assume that
A1: f is_differentiable_on ].p,g.[ and
A2: ( for x0 being Real st x0 in ].p,g.[ holds
0 < diff f,x0 or for x0 being Real st x0 in ].p,g.[ holds
diff f,x0 < 0 ) ; :: thesis: rng (f | ].p,g.[) is open
A3: f | ].p,g.[ is continuous by A1, FDIFF_1:33;

now

per cases ( for x0 being Real st x0 in ].p,g.[ holds
0 < diff f,x0 or for x0 being Real st x0 in ].p,g.[ holds
diff f,x0 < 0 ) by A2;

suppose A4: for x0 being Real st x0 in ].p,g.[ holds
0 < diff f,x0 ; :: thesis: rng (f | ].p,g.[) is open

now

per cases ( ].p,g.[ <> {} or ].p,g.[ = {} ) ;

suppose ].p,g.[ <> {} ; :: thesis: f | ].p,g.[ is increasing

then p < g by XXREAL_1:28;
hence f | ].p,g.[ is increasing by A1, A4, Z, ROLLE:9; :: thesis: verum

end;

suppose ].p,g.[ = {} ; :: thesis: f | ].p,g.[ is increasing

then for r1, r2 being Real st r1 in ].p,g.[ /\ (dom f) & r2 in ].p,g.[ /\ (dom f) & r1 < r2 holds
f . r1 < f . r2 ;
hence f | ].p,g.[ is increasing by RFUNCT_2:43; :: thesis: verum

end;

end;

end;

hence rng (f | ].p,g.[) is open by A3, Z, FCONT_3:31; :: thesis: verum

end;

suppose A5: for x0 being Real st x0 in ].p,g.[ holds
diff f,x0 < 0 ; :: thesis: rng (f | ].p,g.[) is open

now

per cases ( ].p,g.[ <> {} or ].p,g.[ = {} ) ;

suppose ].p,g.[ <> {} ; :: thesis: f | ].p,g.[ is decreasing

then p < g by XXREAL_1:28;
hence f | ].p,g.[ is decreasing by A1, A5, Z, ROLLE:10; :: thesis: verum

end;

suppose ].p,g.[ = {} ; :: thesis: f | ].p,g.[ is decreasing

then for r1, r2 being Real st r1 in ].p,g.[ /\ (dom f) & r2 in ].p,g.[ /\ (dom f) & r1 < r2 holds
f . r2 < f . r1 ;
hence f | ].p,g.[ is decreasing by RFUNCT_2:44; :: thesis: verum

end;

end;

end;

hence rng (f | ].p,g.[) is open by A3, Z, FCONT_3:31; :: thesis: verum

end;

end;

end;

hence rng (f | ].p,g.[) is open ; :: thesis: verum