let f be PartFunc of REAL,REAL; :: thesis: ( [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff (f,x0) or for x0 being Real holds diff (f,x0) < 0 ) implies rng f is open )
assume A1: [#] REAL c= dom f ; :: thesis: ( not f is_differentiable_on [#] REAL or ( not for x0 being Real holds 0 < diff (f,x0) & not for x0 being Real holds diff (f,x0) < 0 ) or rng f is open )
assume that
A2: f is_differentiable_on [#] REAL and
A3: ( for x0 being Real holds 0 < diff (f,x0) or for x0 being Real holds diff (f,x0) < 0 ) ; :: thesis: rng f is open
A4: f | ([#] REAL) is continuous by A2, FDIFF_1:25;

now :: thesis: rng f is open

per cases ( for x0 being Real holds 0 < diff (f,x0) or for x0 being Real holds diff (f,x0) < 0 ) by A3;

suppose for x0 being Real holds 0 < diff (f,x0) ; :: thesis: rng f is open

then f | ([#] REAL) is increasing by A2, Th37;
hence rng f is open by A1, A4, FCONT_3:26; :: thesis: verum

end;

suppose for x0 being Real holds diff (f,x0) < 0 ; :: thesis: rng f is open

then f | ([#] REAL) is decreasing by A2, Th38;
hence rng f is open by A1, A4, FCONT_3:26; :: thesis: verum

end;

end;

end;

hence rng f is open ; :: thesis: verum