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;
end;
end;
hence rng f is open ; :: thesis: verum