:: FCONT_1 semantic presentation

begin

definition
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
let x0 be ( ( real ) ( V22() real ext-real ) number ) ;
pred f is_continuous_in x0 means :: FCONT_1:def 1
 for s1 being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st rng s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( non empty V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) c= dom f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = x0 : ( ( ) ( ) set ) holds
( f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) /* s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is convergent & f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) . x0 : ( ( ) ( ) set ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V34() ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = lim (f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) /* s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) );
end;

theorem :: FCONT_1:1
for X being ( ( ) ( ) set )
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st x0 : ( ( real ) ( V22() real ext-real ) number ) in X : ( ( ) ( ) set ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FCONT_1:2
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) iff for s1 being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st rng s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( non empty V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) holds s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) <> x0 : ( ( real ) ( V22() real ext-real ) number ) ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is convergent & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = lim (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ) ;

theorem :: FCONT_1:3
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) iff for r being ( ( real ) ( V22() real ext-real ) number ) st 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) holds
ex s being ( ( real ) ( V22() real ext-real ) number ) st
( 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) < s : ( ( real ) ( V22() real ext-real ) number ) & ( for x1 being ( ( real ) ( V22() real ext-real ) number ) st x1 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & abs (x1 : ( ( real ) ( V22() real ext-real ) number ) - x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) < s : ( ( real ) ( V22() real ext-real ) number ) holds
abs ((f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) - (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) < r : ( ( real ) ( V22() real ext-real ) number ) ) ) ) ;

theorem :: FCONT_1:4
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for x0 being ( ( real ) ( V22() real ext-real ) number ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) iff for N1 being ( ( ) ( V45() V46() V47() open ) Neighbourhood of f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ex N being ( ( ) ( V45() V46() V47() open ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) st
for x1 being ( ( real ) ( V22() real ext-real ) number ) st x1 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & x1 : ( ( real ) ( V22() real ext-real ) number ) in N : ( ( ) ( V45() V46() V47() open ) Neighbourhood of b2 : ( ( real ) ( V22() real ext-real ) number ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) in N1 : ( ( ) ( V45() V46() V47() open ) Neighbourhood of b1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . b2 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ) ;

theorem :: FCONT_1:5
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for x0 being ( ( real ) ( V22() real ext-real ) number ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) iff for N1 being ( ( ) ( V45() V46() V47() open ) Neighbourhood of f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ex N being ( ( ) ( V45() V46() V47() open ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: N : ( ( ) ( V45() V46() V47() open ) Neighbourhood of b2 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) c= N1 : ( ( ) ( V45() V46() V47() open ) Neighbourhood of b1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . b2 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ) ;

theorem :: FCONT_1:6
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ex N being ( ( ) ( V45() V46() V47() open ) Neighbourhood of x0 : ( ( real ) ( V22() real ext-real ) number ) ) st (dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) /\ N : ( ( ) ( V45() V46() V47() open ) Neighbourhood of b1 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = {x0 : ( ( real ) ( V22() real ext-real ) number ) } : ( ( ) ( non empty trivial V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FCONT_1:7
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st x0 : ( ( real ) ( V22() real ext-real ) number ) in (dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) /\ (dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
( f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ) ;

theorem :: FCONT_1:8
for x0, r being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
r : ( ( real ) ( V22() real ext-real ) number ) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FCONT_1:9
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
( abs f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) & - f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ) ;

theorem :: FCONT_1:10
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FCONT_1:11
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f2, f1 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) / f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FCONT_1:12
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f2, f1 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom (f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) * f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) holds
f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) * f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;

definition
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
attr f is continuous means :: FCONT_1:def 2
 for x0 being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) ;
end;

theorem :: FCONT_1:13
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous iff for s1 being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st rng s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( non empty V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) c= X : ( ( ) ( ) set ) & s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) in X : ( ( ) ( ) set ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is convergent & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . (lim s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = lim (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* s1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ) ;

theorem :: FCONT_1:14
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous iff for x0, r being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in X : ( ( ) ( ) set ) & 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) holds
ex s being ( ( real ) ( V22() real ext-real ) number ) st
( 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) < s : ( ( real ) ( V22() real ext-real ) number ) & ( for x1 being ( ( real ) ( V22() real ext-real ) number ) st x1 : ( ( real ) ( V22() real ext-real ) number ) in X : ( ( ) ( ) set ) & abs (x1 : ( ( real ) ( V22() real ext-real ) number ) - x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) < s : ( ( real ) ( V22() real ext-real ) number ) holds
abs ((f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) - (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) < r : ( ( real ) ( V22() real ext-real ) number ) ) ) ) ;

registration
cluster Function-like V8() -> Function-like continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let f be ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;
cluster f : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:15
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous iff (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ) ;

theorem :: FCONT_1:16
for X, X1 being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & X1 : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

registration
cluster Function-like empty -> Function-like continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
let X be ( ( trivial ) ( trivial ) set ) ;
cluster f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( trivial ) ( trivial ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( trivial ) ( trivial ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:17
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | {x0 : ( ( real ) ( V22() real ext-real ) number ) } : ( ( ) ( non empty trivial V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined {b1 : ( ( real ) ( V22() real ext-real ) number ) } : ( ( ) ( non empty trivial V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

registration
let f1, f2 be ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) PartFunc of ,) ;
cluster f1 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + f2 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster f1 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) - f2 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster f1 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) (#) f2 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:18
for X being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= (dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) /\ (dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
( (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ) ;

theorem :: FCONT_1:19
for X, X1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & X1 : ( ( ) ( ) set ) c= dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
( (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ) ;

registration
let f be ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) PartFunc of ,) ;
let r be ( ( real ) ( V22() real ext-real ) number ) ;
cluster r : ( ( real ) ( V22() real ext-real ) set ) (#) f : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:20
for r being ( ( real ) ( V22() real ext-real ) number )
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
(r : ( ( real ) ( V22() real ext-real ) number ) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:21
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
( (abs f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & (- f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ) ;

theorem :: FCONT_1:22
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty trivial V45() V46() V47() V48() V49() V50() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) set ) holds
(f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:23
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty trivial V45() V46() V47() V48() V49() V50() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) set ) holds
(f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:24
for X being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= (dom f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) /\ (dom f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty trivial V45() V46() V47() V48() V49() V50() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) set ) & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
(f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) / f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

registration
let f1, f2 be ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) PartFunc of ,) ;
cluster f1 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) (#) f2 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued continuous ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:25
for X being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: X : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined b2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: b1 : ( ( ) ( ) set ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
(f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) * f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:26
for X, X1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
(f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) * f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ (f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) " X1 : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) /\ (b3 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) " b2 : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:27
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & ( for x1, x2 being ( ( real ) ( V22() real ext-real ) number ) holds f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . (x1 : ( ( real ) ( V22() real ext-real ) number ) + x2 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) + (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x2 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) & ex x0 being ( ( real ) ( V22() real ext-real ) number ) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:28
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) is compact & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | (dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined dom b1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
rng f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) is compact ;

theorem :: FCONT_1:29
for Y being ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) is compact & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) is compact ;

theorem :: FCONT_1:30
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) <> {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) set ) & dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) is compact & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | (dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined dom b1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
ex x1, x2 being ( ( real ) ( V22() real ext-real ) number ) st
( x1 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & x2 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = upper_bound (rng f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x2 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = lower_bound (rng f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ;

theorem :: FCONT_1:31
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued 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 ) ) <> {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) set ) & Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) is compact & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous holds
ex x1, x2 being ( ( real ) ( V22() real ext-real ) number ) st
( x1 : ( ( real ) ( V22() real ext-real ) number ) in Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) & x2 : ( ( real ) ( V22() real ext-real ) number ) in Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = upper_bound (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x2 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = lower_bound (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ;

definition
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
attr f is Lipschitzian means :: FCONT_1:def 3
 ex r being ( ( real ) ( V22() real ext-real ) number ) st
( 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) & ( for x1, x2 being ( ( real ) ( V22() real ext-real ) number ) st x1 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( ) ( ) set ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & x2 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( ) ( ) set ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
abs ((f : ( ( ) ( ) set ) . x1 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) - (f : ( ( ) ( ) set ) . x2 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) <= r : ( ( real ) ( V22() real ext-real ) number ) * (abs (x1 : ( ( real ) ( V22() real ext-real ) number ) - x2 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) );
end;

theorem :: FCONT_1:32
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian iff ex r being ( ( real ) ( V22() real ext-real ) number ) st
( 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V22() real ext-real ) number ) & ( for x1, x2 being ( ( real ) ( V22() real ext-real ) number ) st x1 : ( ( real ) ( V22() real ext-real ) number ) in dom (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & x2 : ( ( real ) ( V22() real ext-real ) number ) in dom (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
abs ((f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x1 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) - (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x2 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) <= r : ( ( real ) ( V22() real ext-real ) number ) * (abs (x1 : ( ( real ) ( V22() real ext-real ) number ) - x2 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) ) ) ;

registration
cluster Function-like empty -> Function-like Lipschitzian for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like empty complex-valued ext-real-valued real-valued for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let f be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;
cluster f : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:33
for X, X1 being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & X1 : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

registration
let f1, f2 be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) PartFunc of ,) ;
cluster f1 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + f2 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster f1 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) - f2 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:34
for X, X1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian holds
(f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

theorem :: FCONT_1:35
for X, X1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian holds
(f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

registration
let f1, f2 be ( ( Function-like bounded Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Lipschitzian ) PartFunc of ,) ;
cluster f1 : ( ( Function-like bounded Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) (#) f2 : ( ( Function-like bounded Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:36
for X, X1, Z, Z1 being ( ( ) ( ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Z : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is bounded & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Z1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b4 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is bounded holds
(f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (((X : ( ( ) ( ) set ) /\ Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ Z1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like ((b1 : ( ( ) ( ) set ) /\ b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ b4 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

registration
let f be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) PartFunc of ,) ;
let p be ( ( real ) ( V22() real ext-real ) number ) ;
cluster p : ( ( real ) ( V22() real ext-real ) set ) (#) f : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:37
for X being ( ( ) ( ) set )
for p being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
(p : ( ( real ) ( V22() real ext-real ) number ) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

registration
let f be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) PartFunc of ,) ;
cluster |.f : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) .| : ( ( Relation-like Function-like real-valued ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: FCONT_1:38
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian holds
( - (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & (abs f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ) ;

registration
cluster Function-like V8() -> Function-like Lipschitzian for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let Y be ( ( ) ( V45() V46() V47() ) Subset of ( ( ) ( ) set ) ) ;
cluster id Y : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Y : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined Y : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -valued Function-like one-to-one total complex-valued ext-real-valued real-valued ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

registration
cluster Function-like Lipschitzian -> Function-like continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: FCONT_1:39
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ex r being ( ( real ) ( V22() real ext-real ) number ) st rng f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = {r : ( ( real ) ( V22() real ext-real ) number ) } : ( ( ) ( non empty trivial V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is continuous ;

theorem :: FCONT_1:40
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ( for x0 being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is continuous ;

theorem :: FCONT_1:41
for X being ( ( ) ( ) set )
for r, p being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ( for x0 being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = (r : ( ( real ) ( V22() real ext-real ) number ) * x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) + p : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:42
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ( for x0 being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) ^2 : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | (dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined dom b1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:43
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & ( for x0 being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = x0 : ( ( real ) ( V22() real ext-real ) number ) ^2 : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:44
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ( for x0 being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = abs x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is continuous ;

theorem :: FCONT_1:45
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ( for x0 being ( ( real ) ( V22() real ext-real ) number ) st x0 : ( ( real ) ( V22() real ext-real ) number ) in X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = abs x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:46
for X being ( ( ) ( ) set )
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is monotone & ex p, g being ( ( real ) ( V22() real ext-real ) number ) st
( p : ( ( real ) ( V22() real ext-real ) number ) <= g : ( ( real ) ( V22() real ext-real ) number ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: X : ( ( ) ( ) set ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = [.p : ( ( real ) ( V22() real ext-real ) number ) ,g : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: FCONT_1:47
for p, g being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) st p : ( ( real ) ( V22() real ext-real ) number ) <= g : ( ( real ) ( V22() real ext-real ) number ) & [.p : ( ( real ) ( V22() real ext-real ) number ) ,g : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) & ( f : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( real ) ( V22() real ext-real ) number ) ,g : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined [.b1 : ( ( real ) ( V22() real ext-real ) number ) ,b2 : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing or f : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( real ) ( V22() real ext-real ) number ) ,g : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined [.b1 : ( ( real ) ( V22() real ext-real ) number ) ,b2 : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ) holds
((f : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( real ) ( V22() real ext-real ) number ) ,g : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined [.b1 : ( ( real ) ( V22() real ext-real ) number ) ,b2 : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (f : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( real ) ( V22() real ext-real ) number ) ,g : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined b3 : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.b1 : ( ( real ) ( V22() real ext-real ) number ) ,b2 : ( ( real ) ( V22() real ext-real ) number ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous ;

definition
let a, b be ( ( real ) ( V22() real ext-real ) number ) ;
func AffineMap (a,b) -> ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) means :: FCONT_1:def 4
 for x being ( ( real ) ( V22() real ext-real ) number ) holds it : ( ( Function-like ) ( Relation-like a : ( ( ) ( ) set ) -defined b : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:a : ( ( ) ( ) set ) ,b : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = (a : ( ( ) ( ) set ) * x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( ) set ) + b : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) ;
end;

registration
let a, b be ( ( real ) ( V22() real ext-real ) number ) ;
cluster AffineMap (a : ( ( real ) ( V22() real ext-real ) set ) ,b : ( ( real ) ( V22() real ext-real ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) -> Function-like quasi_total continuous ;
end;

registration
cluster Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ,REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: FCONT_1:48
for a, b being ( ( real ) ( V22() real ext-real ) number ) holds (AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = b : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: FCONT_1:49
for a, b being ( ( real ) ( V22() real ext-real ) number ) holds (AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V64() V66() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) = a : ( ( real ) ( V22() real ext-real ) number ) + b : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) set ) ;

theorem :: FCONT_1:50
for a, b being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) holds
AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) is one-to-one ;

theorem :: FCONT_1:51
for a, b, x, y being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) > 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) & x : ( ( real ) ( V22() real ext-real ) number ) < y : ( ( real ) ( V22() real ext-real ) number ) holds
(AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) < (AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . y : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ;

theorem :: FCONT_1:52
for a, b, x, y being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) < 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) & x : ( ( real ) ( V22() real ext-real ) number ) < y : ( ( real ) ( V22() real ext-real ) number ) holds
(AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) > (AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . y : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ;

theorem :: FCONT_1:53
for a, b, x, y being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) >= 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) & x : ( ( real ) ( V22() real ext-real ) number ) <= y : ( ( real ) ( V22() real ext-real ) number ) holds
(AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) <= (AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . y : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ;

theorem :: FCONT_1:54
for a, b, x, y being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) <= 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) & x : ( ( real ) ( V22() real ext-real ) number ) <= y : ( ( real ) ( V22() real ext-real ) number ) holds
(AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) >= (AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) . y : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ;

theorem :: FCONT_1:55
for a, b being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) holds
rng (AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) : ( ( ) ( non empty V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ;

theorem :: FCONT_1:56
for a, b being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) holds
(AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) " : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = AffineMap ((a : ( ( real ) ( V22() real ext-real ) number ) ") : ( ( V22() ) ( V22() real ext-real ) set ) ,(- (b : ( ( real ) ( V22() real ext-real ) number ) / a : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of COMPLEX : ( ( ) ( non empty V45() V51() V52() ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) ;

theorem :: FCONT_1:57
for a, b being ( ( real ) ( V22() real ext-real ) number ) st a : ( ( real ) ( V22() real ext-real ) number ) > 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) holds
(AffineMap (a : ( ( real ) ( V22() real ext-real ) number ) ,b : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( Function-like quasi_total ) ( Relation-like REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Function of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) ) .: [.0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V45() V46() V47() V48() V51() V52() ) set ) -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V64() V66() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V45() V46() V47() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) = [.b : ( ( real ) ( V22() real ext-real ) number ) ,(a : ( ( real ) ( V22() real ext-real ) number ) + b : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) .] : ( ( ) ( V45() V46() V47() V69() closed ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() V66() V67() V69() ) set ) : ( ( ) ( ) set ) ) ;