for p, g being ( ( ) ( V22() real ext-real ) Real) st p : ( ( ) ( V22() real ext-real ) Real) < g : ( ( ) ( V22() real ext-real ) Real) holds
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
ex x0 being ( ( ) ( V22() real ext-real ) Real) st
( x0 : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for x, t being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) < t : ( ( ) ( V22() real ext-real ) Real) holds
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . (x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
ex s being ( ( ) ( V22() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V22() real ext-real ) Real) & s : ( ( ) ( V22() real ext-real ) Real) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) & diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,(x : ( ( ) ( V22() real ext-real ) Real) + (s : ( ( ) ( V22() real ext-real ) Real) * t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for p, g being ( ( ) ( V22() real ext-real ) Real) st p : ( ( ) ( V22() real ext-real ) Real) < g : ( ( ) ( V22() real ext-real ) Real) holds
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
ex x0 being ( ( ) ( V22() real ext-real ) Real) st
( x0 : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = ((f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) - (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) / (g : ( ( ) ( V22() real ext-real ) Real) - p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) ;

for x, t being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) < t : ( ( ) ( V22() real ext-real ) Real) holds
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
ex s being ( ( ) ( V22() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V22() real ext-real ) Real) & s : ( ( ) ( V22() real ext-real ) Real) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . (x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) + (t : ( ( ) ( V22() real ext-real ) Real) * (diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,(x : ( ( ) ( V22() real ext-real ) Real) + (s : ( ( ) ( V22() real ext-real ) Real) * t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) ;

for p, g being ( ( ) ( V22() real ext-real ) Real) st p : ( ( ) ( V22() real ext-real ) Real) < g : ( ( ) ( V22() real ext-real ) Real) holds
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
ex x0 being ( ( ) ( V22() real ext-real ) Real) st
( x0 : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & ((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) - (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) * (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = ((f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) - (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) * (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V22() real ext-real ) Real) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) ;

for x, t being ( ( ) ( V22() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) < t : ( ( ) ( V22() real ext-real ) Real) holds
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .] : ( ( ) ( V47() V48() V49() V68() closed ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x1 being ( ( ) ( V22() real ext-real ) Real) st x1 : ( ( ) ( V22() real ext-real ) Real) in ].x : ( ( ) ( V22() real ext-real ) Real) ,(x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x1 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) <> 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
ex s being ( ( ) ( V22() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V22() real ext-real ) Real) & s : ( ( ) ( V22() real ext-real ) Real) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() left_end bounded_below ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) & ((f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . (x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) - (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) / ((f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . (x : ( ( ) ( V22() real ext-real ) Real) + t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) - (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = (diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,(x : ( ( ) ( V22() real ext-real ) Real) + (s : ( ( ) ( V22() real ext-real ) Real) * t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) / (diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,(x : ( ( ) ( V22() real ext-real ) Real) + (s : ( ( ) ( V22() real ext-real ) Real) * t : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) ;

for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is V8() ;

for p, g being ( ( ) ( V22() real ext-real ) Real)
for f1, f2 being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
diff (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = diff (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) holds
( (f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is V8() & ex r being ( ( ) ( V22() real ext-real ) Real) st
for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) = (f2 : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) + r : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) ;

for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) < diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is increasing ;

for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) < 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is decreasing ;

for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) st ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V47() V48() V49() ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) is_differentiable_on ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) holds
0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() V52() V53() bounded_below V68() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) ) <= diff (f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) ) holds
f : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) PartFunc of ,) | ].p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( V47() V48() V49() non left_end non right_end V68() open ) Element of K19(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V5( REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() non bounded_below non bounded_above V68() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is non-decreasing ;