:: FCONT_2 semantic presentation

begin

definition
let f be ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
attr f is uniformly_continuous means :: FCONT_2:def 1
 for r 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 V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V22() real ext-real ) Real) 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 V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V22() real ext-real ) Real) & ( for x1, x2 being ( ( ) ( V22() real ext-real ) Real) st x1 : ( ( ) ( V22() real ext-real ) Real) in dom f : ( ( V1() Function-like natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) ) Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & x2 : ( ( ) ( V22() real ext-real ) Real) in dom f : ( ( V1() Function-like natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) ) Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & abs (x1 : ( ( ) ( V22() real ext-real ) Real) - x2 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) < s : ( ( ) ( V22() real ext-real ) Real) holds
abs ((f : ( ( V1() Function-like natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) ) Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) . x1 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V34() ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) - (f : ( ( V1() Function-like natural-valued ) ( V1() V5( RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) ) Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) . x2 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V34() ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) < r : ( ( ) ( V22() real ext-real ) Real) ) );
end;

theorem :: FCONT_2:1
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous iff for r 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 V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V22() real ext-real ) Real) 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 V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() left_end bounded_below ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V22() real ext-real ) Real) & ( for x1, x2 being ( ( ) ( V22() real ext-real ) Real) st x1 : ( ( ) ( V22() real ext-real ) Real) in dom (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & x2 : ( ( ) ( V22() real ext-real ) Real) in dom (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & abs (x1 : ( ( ) ( V22() real ext-real ) Real) - x2 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) < s : ( ( ) ( V22() real ext-real ) Real) holds
abs ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) - (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x2 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) < r : ( ( ) ( V22() real ext-real ) Real) ) ) ) ;

theorem :: FCONT_2:2
for X, X1 being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous & X1 : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:3
for X, X1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & X1 : ( ( ) ( ) set ) c= dom f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous & f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
(f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:4
for X, X1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & X1 : ( ( ) ( ) set ) c= dom f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous & f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
(f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:5
for X being ( ( ) ( ) set )
for p being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
(p : ( ( ) ( V22() real ext-real ) Real) (#) f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:6
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
(- f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:7
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
(abs f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:8
for X, X1, Z, Z1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & X1 : ( ( ) ( ) set ) c= dom f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous & f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous & f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Z : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded & f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Z1 : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded holds
(f1 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (((X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ Z1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:9
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_2:10
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is Lipschitzian holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:11
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for Y being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) st Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) is compact & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:12
for Y being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) is compact & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) is compact ;

theorem :: FCONT_2:13
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for Y being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) st Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) <> {} : ( ( ) ( 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() bounded_below V69() ) set ) & Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) is compact & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous holds
ex x1, x2 being ( ( ) ( V22() real ext-real ) Real) st
( x1 : ( ( ) ( V22() real ext-real ) Real) in Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) & x2 : ( ( ) ( V22() real ext-real ) Real) in Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) = upper_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x2 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) = lower_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ) ;

theorem :: FCONT_2:14
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is V8() holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is uniformly_continuous ;

theorem :: FCONT_2:15
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st p : ( ( ) ( V22() real ext-real ) Real) <= g : ( ( ) ( V22() real ext-real ) Real) & [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous holds
for r being ( ( ) ( V22() real ext-real ) Real) st r : ( ( ) ( V22() real ext-real ) Real) in [.(f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ,(f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) \/ [.(f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ,(f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) holds
ex s being ( ( ) ( V22() real ext-real ) Real) st
( s : ( ( ) ( V22() real ext-real ) Real) in [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & r : ( ( ) ( V22() real ext-real ) Real) = f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . s : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ) ;

theorem :: FCONT_2:16
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st p : ( ( ) ( V22() real ext-real ) Real) <= g : ( ( ) ( V22() real ext-real ) Real) & [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous holds
for r being ( ( ) ( V22() real ext-real ) Real) st r : ( ( ) ( V22() real ext-real ) Real) in [.(lower_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ,(upper_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) holds
ex s being ( ( ) ( V22() real ext-real ) Real) st
( s : ( ( ) ( V22() real ext-real ) Real) in [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & r : ( ( ) ( V22() real ext-real ) Real) = f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . s : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ) ;

theorem :: FCONT_2:17
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is one-to-one & [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & p : ( ( ) ( V22() real ext-real ) Real) <= g : ( ( ) ( V22() real ext-real ) Real) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & not f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is increasing holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: FCONT_2:18
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is one-to-one & p : ( ( ) ( V22() real ext-real ) Real) <= g : ( ( ) ( V22() real ext-real ) Real) & [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous & not ( lower_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) = f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) & upper_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) = f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ) holds
( lower_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) = f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . g : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) & upper_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) = f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . p : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ) ;

theorem :: FCONT_2:19
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st p : ( ( ) ( V22() real ext-real ) Real) <= g : ( ( ) ( V22() real ext-real ) Real) & [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) = [.(lower_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ,(upper_bound (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: FCONT_2:20
for p, g being ( ( ) ( V22() real ext-real ) Real)
for f being ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) st p : ( ( ) ( V22() real ext-real ) Real) <= g : ( ( ) ( V22() real ext-real ) Real) & [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous holds
(f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | [.(lower_bound (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) ,(upper_bound (f : ( ( Function-like one-to-one ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Real) ,g : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) .] : ( ( ) ( V45() V46() V47() V69() ) Element of K19(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) V5( REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous ;