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:33;

now

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 A1, A2, Th37;
hence rng f is open by A1, A4, FCONT_3:34; :: thesis: verum

end;

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

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

end;

end;

end;

hence rng f is open ; :: thesis: verum