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

now

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

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

then f | (left_open_halfline p) is increasing by A1, Th29, Z;
hence rng (f | (left_open_halfline p)) is open by A3, Z, FCONT_3:32; :: thesis: verum

end;

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

then f | (left_open_halfline p) is decreasing by A1, Th30, Z;
hence rng (f | (left_open_halfline p)) is open by A3, Z, FCONT_3:32; :: thesis: verum

end;

end;

end;

hence rng (f | (left_open_halfline p)) is open ; :: thesis: verum