let g, p 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 A1: ].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
A2: f is_differentiable_on ].p,g.[ and
A3: ( 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
A4: f | ].p,g.[ is continuous by A2, FDIFF_1:25;

now :: thesis: rng (f | ].p,g.[) is open

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 A3;

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

then f | ].p,g.[ is increasing by A2, ROLLE:9;
hence rng (f | ].p,g.[) is open by A1, A4, FCONT_3:23; :: thesis: verum

end;

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

then f | ].p,g.[ is decreasing by A2, ROLLE:10;
hence rng (f | ].p,g.[) is open by A1, A4, FCONT_3:23; :: thesis: verum

end;

end;

end;

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