let g, p be Real; :: thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f | ].p,g.[ is continuous & ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) holds

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

let f be PartFunc of REAL,REAL; :: thesis: ( ].p,g.[ c= dom f & f | ].p,g.[ is continuous & ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) implies rng (f | ].p,g.[) is open )

assume that

A1: ].p,g.[ c= dom f and

A2: f | ].p,g.[ is continuous and

A3: ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) ; :: thesis: rng (f | ].p,g.[) is open

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

let f be PartFunc of REAL,REAL; :: thesis: ( ].p,g.[ c= dom f & f | ].p,g.[ is continuous & ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) implies rng (f | ].p,g.[) is open )

assume that

A1: ].p,g.[ c= dom f and

A2: f | ].p,g.[ is continuous and

A3: ( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing ) ; :: thesis: rng (f | ].p,g.[) is open

now :: thesis: for r1 being Element of REAL st r1 in rng (f | ].p,g.[) holds

ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[)

hence
rng (f | ].p,g.[) is open
by RCOMP_1:20; :: thesis: verumex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[)

let r1 be Element of REAL ; :: thesis: ( r1 in rng (f | ].p,g.[) implies ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[) )

set f1 = f | ].p,g.[;

assume r1 in rng (f | ].p,g.[) ; :: thesis: ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[)

then consider x0 being Element of REAL such that

A4: x0 in dom (f | ].p,g.[) and

A5: (f | ].p,g.[) . x0 = r1 by PARTFUN1:3;

A6: r1 = f . x0 by A4, A5, FUNCT_1:47;

A7: x0 in (dom f) /\ ].p,g.[ by A4, RELAT_1:61;

then x0 in ].p,g.[ by XBOOLE_0:def 4;

then consider N being Neighbourhood of x0 such that

A8: N c= ].p,g.[ by RCOMP_1:18;

consider r being Real such that

A9: 0 < r and

A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;

reconsider r = r as Element of REAL by XREAL_0:def 1;

0 < r / 2 by A9, XREAL_1:215;

then A11: x0 - (r / 2) < x0 - 0 by XREAL_1:15;

A12: r / 2 < r by A9, XREAL_1:216;

then A13: x0 - r < x0 - (r / 2) by XREAL_1:15;

A14: N c= dom f by A1, A8;

set fp = f . (x0 + (r / 2));

set fm = f . (x0 - (r / 2));

A15: x0 + (r / 2) < x0 + r by A12, XREAL_1:8;

A16: x0 < x0 + (r / 2) by A9, XREAL_1:29, XREAL_1:215;

then A17: x0 - (r / 2) < x0 + (r / 2) by A11, XXREAL_0:2;

x0 < x0 + r by A9, XREAL_1:29;

then x0 - (r / 2) < x0 + r by A11, XXREAL_0:2;

then A18: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A13;

then A19: x0 - (r / 2) in ].p,g.[ /\ (dom f) by A8, A10, A14, XBOOLE_0:def 4;

x0 - r < x0 by A9, XREAL_1:44;

then x0 - r < x0 + (r / 2) by A16, XXREAL_0:2;

then A20: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A15;

then A21: x0 + (r / 2) in ].p,g.[ /\ (dom f) by A8, A10, A14, XBOOLE_0:def 4;

A22: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A18, A20, XXREAL_2:def 12;

A23: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].p,g.[ by A8, A10, A18, A20, XXREAL_2:def 12;

then A24: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A2, FCONT_1:16;

end;set f1 = f | ].p,g.[;

assume r1 in rng (f | ].p,g.[) ; :: thesis: ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[)

then consider x0 being Element of REAL such that

A4: x0 in dom (f | ].p,g.[) and

A5: (f | ].p,g.[) . x0 = r1 by PARTFUN1:3;

A6: r1 = f . x0 by A4, A5, FUNCT_1:47;

A7: x0 in (dom f) /\ ].p,g.[ by A4, RELAT_1:61;

then x0 in ].p,g.[ by XBOOLE_0:def 4;

then consider N being Neighbourhood of x0 such that

A8: N c= ].p,g.[ by RCOMP_1:18;

consider r being Real such that

A9: 0 < r and

A10: N = ].(x0 - r),(x0 + r).[ by RCOMP_1:def 6;

reconsider r = r as Element of REAL by XREAL_0:def 1;

0 < r / 2 by A9, XREAL_1:215;

then A11: x0 - (r / 2) < x0 - 0 by XREAL_1:15;

A12: r / 2 < r by A9, XREAL_1:216;

then A13: x0 - r < x0 - (r / 2) by XREAL_1:15;

A14: N c= dom f by A1, A8;

set fp = f . (x0 + (r / 2));

set fm = f . (x0 - (r / 2));

A15: x0 + (r / 2) < x0 + r by A12, XREAL_1:8;

A16: x0 < x0 + (r / 2) by A9, XREAL_1:29, XREAL_1:215;

then A17: x0 - (r / 2) < x0 + (r / 2) by A11, XXREAL_0:2;

x0 < x0 + r by A9, XREAL_1:29;

then x0 - (r / 2) < x0 + r by A11, XXREAL_0:2;

then A18: x0 - (r / 2) in ].(x0 - r),(x0 + r).[ by A13;

then A19: x0 - (r / 2) in ].p,g.[ /\ (dom f) by A8, A10, A14, XBOOLE_0:def 4;

x0 - r < x0 by A9, XREAL_1:44;

then x0 - r < x0 + (r / 2) by A16, XXREAL_0:2;

then A20: x0 + (r / 2) in ].(x0 - r),(x0 + r).[ by A15;

then A21: x0 + (r / 2) in ].p,g.[ /\ (dom f) by A8, A10, A14, XBOOLE_0:def 4;

A22: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].(x0 - r),(x0 + r).[ by A18, A20, XXREAL_2:def 12;

A23: [.(x0 - (r / 2)),(x0 + (r / 2)).] c= ].p,g.[ by A8, A10, A18, A20, XXREAL_2:def 12;

then A24: f | [.(x0 - (r / 2)),(x0 + (r / 2)).] is continuous by A2, FCONT_1:16;

now :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | ].p,g.[)end;

hence
ex N being Neighbourhood of r1 st N c= rng (f | ].p,g.[)
; :: thesis: verumper cases
( f | ].p,g.[ is increasing or f | ].p,g.[ is decreasing )
by A3;

end;

suppose A25:
f | ].p,g.[ is increasing
; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | ].p,g.[)

set R = min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)));

f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20;

then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;

f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20;

then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;

then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15;

then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def 6;

take N1 = N1; :: thesis: N1 c= rng (f | ].p,g.[)

f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20;

then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;

then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;

thus N1 c= rng (f | ].p,g.[) :: thesis: verum

end;f . x0 < f . (x0 + (r / 2)) by A7, A16, A21, A25, RFUNCT_2:20;

then A26: 0 < (f . (x0 + (r / 2))) - (f . x0) by XREAL_1:50;

f . (x0 - (r / 2)) < f . x0 by A7, A11, A19, A25, RFUNCT_2:20;

then 0 < (f . x0) - (f . (x0 - (r / 2))) by XREAL_1:50;

then 0 < min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) by A26, XXREAL_0:15;

then reconsider N1 = ].(r1 - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))),(r1 + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))))).[ as Neighbourhood of r1 by RCOMP_1:def 6;

take N1 = N1; :: thesis: N1 c= rng (f | ].p,g.[)

f . (x0 - (r / 2)) < f . (x0 + (r / 2)) by A17, A21, A19, A25, RFUNCT_2:20;

then [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = {} by XXREAL_1:29;

then A27: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] ;

thus N1 c= rng (f | ].p,g.[) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng (f | ].p,g.[) )

A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25;

assume x in N1 ; :: thesis: x in rng (f | ].p,g.[)

then consider r2 being Real such that

A29: r2 = x and

A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and

A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6;

min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17;

then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;

then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2;

min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17;

then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13;

then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2;

then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32;

then consider s being Real such that

A33: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and

A34: x = f . s by A1, A23, A24, A17, A27, A29, A28, FCONT_2:15, XBOOLE_1:1;

s in N by A10, A22, A33;

then s in (dom f) /\ ].p,g.[ by A8, A14, XBOOLE_0:def 4;

then A35: s in dom (f | ].p,g.[) by RELAT_1:61;

then x = (f | ].p,g.[) . s by A34, FUNCT_1:47;

hence x in rng (f | ].p,g.[) by A35, FUNCT_1:def 3; :: thesis: verum

end;A28: ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ c= [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] by XXREAL_1:25;

assume x in N1 ; :: thesis: x in rng (f | ].p,g.[)

then consider r2 being Real such that

A29: r2 = x and

A30: (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) < r2 and

A31: r2 < (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by A6;

min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . (x0 + (r / 2))) - (f . x0) by XXREAL_0:17;

then (f . x0) + (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) <= (f . x0) + ((f . (x0 + (r / 2))) - (f . x0)) by XREAL_1:7;

then A32: r2 < f . (x0 + (r / 2)) by A31, XXREAL_0:2;

min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0))) <= (f . x0) - (f . (x0 - (r / 2))) by XXREAL_0:17;

then (f . x0) - ((f . x0) - (f . (x0 - (r / 2)))) <= (f . x0) - (min (((f . x0) - (f . (x0 - (r / 2)))),((f . (x0 + (r / 2))) - (f . x0)))) by XREAL_1:13;

then f . (x0 - (r / 2)) < r2 by A30, XXREAL_0:2;

then r2 in ].(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).[ by A32;

then consider s being Real such that

A33: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and

A34: x = f . s by A1, A23, A24, A17, A27, A29, A28, FCONT_2:15, XBOOLE_1:1;

s in N by A10, A22, A33;

then s in (dom f) /\ ].p,g.[ by A8, A14, XBOOLE_0:def 4;

then A35: s in dom (f | ].p,g.[) by RELAT_1:61;

then x = (f | ].p,g.[) . s by A34, FUNCT_1:47;

hence x in rng (f | ].p,g.[) by A35, FUNCT_1:def 3; :: thesis: verum

suppose A36:
f | ].p,g.[ is decreasing
; :: thesis: ex N1 being Neighbourhood of r1 st N1 c= rng (f | ].p,g.[)

set R = min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))));

f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21;

then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;

f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21;

then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;

then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15;

then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def 6;

take N1 = N1; :: thesis: N1 c= rng (f | ].p,g.[)

f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21;

then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;

then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;

thus N1 c= rng (f | ].p,g.[) :: thesis: verum

end;f . (x0 + (r / 2)) < f . x0 by A7, A16, A21, A36, RFUNCT_2:21;

then A37: 0 < (f . x0) - (f . (x0 + (r / 2))) by XREAL_1:50;

f . x0 < f . (x0 - (r / 2)) by A7, A11, A19, A36, RFUNCT_2:21;

then 0 < (f . (x0 - (r / 2))) - (f . x0) by XREAL_1:50;

then 0 < min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) by A37, XXREAL_0:15;

then reconsider N1 = ].(r1 - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))),(r1 + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))))).[ as Neighbourhood of r1 by RCOMP_1:def 6;

take N1 = N1; :: thesis: N1 c= rng (f | ].p,g.[)

f . (x0 + (r / 2)) < f . (x0 - (r / 2)) by A17, A21, A19, A36, RFUNCT_2:21;

then [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] = {} by XXREAL_1:29;

then A38: [.(f . (x0 - (r / 2))),(f . (x0 + (r / 2))).] \/ [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] = [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] ;

thus N1 c= rng (f | ].p,g.[) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N1 or x in rng (f | ].p,g.[) )

A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;

assume x in N1 ; :: thesis: x in rng (f | ].p,g.[)

then consider r2 being Real such that

A40: r2 = x and

A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and

A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6;

min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;

then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;

then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2;

min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17;

then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13;

then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2;

then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43;

then consider s being Real such that

A44: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and

A45: x = f . s by A1, A23, A24, A17, A38, A40, A39, FCONT_2:15, XBOOLE_1:1;

s in N by A10, A22, A44;

then s in (dom f) /\ ].p,g.[ by A8, A14, XBOOLE_0:def 4;

then A46: s in dom (f | ].p,g.[) by RELAT_1:61;

then x = (f | ].p,g.[) . s by A45, FUNCT_1:47;

hence x in rng (f | ].p,g.[) by A46, FUNCT_1:def 3; :: thesis: verum

end;A39: ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ c= [.(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).] by XXREAL_1:25;

assume x in N1 ; :: thesis: x in rng (f | ].p,g.[)

then consider r2 being Real such that

A40: r2 = x and

A41: (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) < r2 and

A42: r2 < (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by A6;

min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . (x0 - (r / 2))) - (f . x0) by XXREAL_0:17;

then (f . x0) + (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) <= (f . x0) + ((f . (x0 - (r / 2))) - (f . x0)) by XREAL_1:7;

then A43: r2 < f . (x0 - (r / 2)) by A42, XXREAL_0:2;

min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2))))) <= (f . x0) - (f . (x0 + (r / 2))) by XXREAL_0:17;

then (f . x0) - ((f . x0) - (f . (x0 + (r / 2)))) <= (f . x0) - (min (((f . (x0 - (r / 2))) - (f . x0)),((f . x0) - (f . (x0 + (r / 2)))))) by XREAL_1:13;

then f . (x0 + (r / 2)) < r2 by A41, XXREAL_0:2;

then r2 in ].(f . (x0 + (r / 2))),(f . (x0 - (r / 2))).[ by A43;

then consider s being Real such that

A44: s in [.(x0 - (r / 2)),(x0 + (r / 2)).] and

A45: x = f . s by A1, A23, A24, A17, A38, A40, A39, FCONT_2:15, XBOOLE_1:1;

s in N by A10, A22, A44;

then s in (dom f) /\ ].p,g.[ by A8, A14, XBOOLE_0:def 4;

then A46: s in dom (f | ].p,g.[) by RELAT_1:61;

then x = (f | ].p,g.[) . s by A45, FUNCT_1:47;

hence x in rng (f | ].p,g.[) by A46, FUNCT_1:def 3; :: thesis: verum