:: FCONT_3 semantic presentation

begin

registration
cluster [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) -> closed ;
cluster empty -> closed for ( ( ) ( ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) -> open ;
cluster empty -> open for ( ( ) ( ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let r be ( ( real ) ( V22() real ext-real ) number ) ;
cluster right_closed_halfline r : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) -> closed ;
cluster left_closed_halfline r : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) -> closed ;
cluster right_open_halfline r : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) -> open ;
cluster halfline r : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) -> open ;
end;

theorem :: FCONT_3:1
for g, x0 being ( ( ) ( V22() real ext-real ) Real)
for r being ( ( real ) ( V22() real ext-real ) number ) st g : ( ( ) ( V22() real ext-real ) Real) in ].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
abs (g : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) < r : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FCONT_3:2
for g, x0 being ( ( ) ( V22() real ext-real ) Real)
for r being ( ( real ) ( V22() real ext-real ) number ) st g : ( ( ) ( V22() real ext-real ) Real) in ].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
g : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) in ].(- r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( V22() ) ( V22() real ext-real ) set ) ,r : ( ( real ) ( V22() real ext-real ) number ) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: FCONT_3:3
for g, x0, r1 being ( ( ) ( V22() real ext-real ) Real)
for r being ( ( real ) ( V22() real ext-real ) number ) st g : ( ( ) ( V22() real ext-real ) Real) = x0 : ( ( ) ( V22() real ext-real ) Real) + r1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) & abs r1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) < r : ( ( real ) ( V22() real ext-real ) number ) holds
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) & g : ( ( ) ( V22() real ext-real ) Real) in ].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: FCONT_3:4
for g, x0 being ( ( ) ( V22() real ext-real ) Real)
for r being ( ( real ) ( V22() real ext-real ) number ) st g : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) in ].(- r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( V22() ) ( V22() real ext-real ) set ) ,r : ( ( real ) ( V22() real ext-real ) number ) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
( 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) & g : ( ( ) ( V22() real ext-real ) Real) in ].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: FCONT_3:5
for p being ( ( ) ( V22() real ext-real ) Real)
for a being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence)
for x0 being ( ( real ) ( V22() real ext-real ) number ) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds a : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) - (p : ( ( ) ( V22() real ext-real ) Real) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V82() V83() V84() V85() V86() V87() V88() V89() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ) holds
( a : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) is convergent & lim a : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) ) ;

theorem :: FCONT_3:6
for p being ( ( ) ( V22() real ext-real ) Real)
for a being ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence)
for x0 being ( ( real ) ( V22() real ext-real ) number ) st ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds a : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) + (p : ( ( ) ( V22() real ext-real ) Real) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V82() V83() V84() V85() V86() V87() V88() V89() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V82() V83() V84() V85() V86() V87() V88() V89() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) ) holds
( a : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) is convergent & lim a : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V84() V85() V86() V87() V88() V89() V90() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) ) ;

theorem :: FCONT_3:7
for x0 being ( ( ) ( V22() real ext-real ) Real)
for r being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_continuous_in x0 : ( ( ) ( V22() real ext-real ) Real) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x0 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) <> r : ( ( real ) ( V22() real ext-real ) number ) & ex N being ( ( ) ( open V84() V85() V86() ) Neighbourhood of x0 : ( ( ) ( V22() real ext-real ) Real) ) st N : ( ( ) ( open V84() V85() V86() ) Neighbourhood of b1 : ( ( ) ( V22() real ext-real ) Real) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
ex N being ( ( ) ( open V84() V85() V86() ) Neighbourhood of x0 : ( ( ) ( V22() real ext-real ) Real) ) st
( N : ( ( ) ( open V84() V85() V86() ) Neighbourhood of b1 : ( ( ) ( V22() real ext-real ) Real) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for g being ( ( ) ( V22() real ext-real ) Real) st g : ( ( ) ( V22() real ext-real ) Real) in N : ( ( ) ( open V84() V85() V86() ) Neighbourhood of b1 : ( ( ) ( V22() real ext-real ) Real) ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) <> r : ( ( real ) ( V22() real ext-real ) number ) ) ) ;

theorem :: FCONT_3:8
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st ( f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is one-to-one ;

theorem :: FCONT_3:9
for X being ( ( ) ( ) set )
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing holds
((f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(b2 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: b1 : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4(b1 : ( ( ) ( ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: FCONT_3:10
for X being ( ( ) ( ) set )
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing holds
((f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(b2 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: b1 : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4(b1 : ( ( ) ( ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: FCONT_3:11
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is monotone & ex p being ( ( ) ( V22() real ext-real ) Real) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:12
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is monotone & ex p being ( ( ) ( V22() real ext-real ) Real) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:13
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is monotone & ex p being ( ( ) ( V22() real ext-real ) Real) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = left_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:14
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is monotone & ex p being ( ( ) ( V22() real ext-real ) Real) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = right_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:15
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is monotone & ex p, g being ( ( ) ( V22() real ext-real ) Real) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:16
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is monotone & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) .: X : ( ( ) ( ) set ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4(b1 : ( ( ) ( ) set ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:17
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st ( f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) & ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
((f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(b3 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: ].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:18
for p being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st ( f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) & left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
((f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(b2 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:19
for p being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st ( f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) & right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
((f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(b2 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:20
for p being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st ( f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (left_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (left_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) & left_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
((f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (left_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (left_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(b2 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (left_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:21
for p being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st ( f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (right_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (right_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) & right_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
((f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | (right_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (right_closed_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(b2 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) .: (right_closed_halfline b1 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( closed V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:22
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) st ( f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | ([#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) | ([#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) & f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) is total holds
(f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | (rng f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( rng b1 : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like one-to-one V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_3:23
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & ( f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) holds
rng (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4(].b1 : ( ( ) ( V22() real ext-real ) Real) ,b2 : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V84() V85() V86() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) is open ;

theorem :: FCONT_3:24
for p being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & ( f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) holds
rng (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (left_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( left_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) is open ;

theorem :: FCONT_3:25
for p being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & ( f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) holds
rng (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | (right_open_halfline p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V4( right_open_halfline b1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) is open ;

theorem :: FCONT_3:26
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | ([#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & ( f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | ([#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | ([#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( [#] REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) : ( ( ) ( closed open V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( V1() V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is decreasing ) holds
rng f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V84() V85() V86() ) Element of K19(REAL : ( ( ) ( non empty V48() V84() V85() V86() V90() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) is open ;