:: NCFCONT2 semantic presentation

begin

definition
let X be ( ( ) ( ) set ) ;
let CNS1, CNS2 be ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of CNS1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of CNS2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NCFCONT2:def 1
( X : ( ( ) ( ) CNORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of CNS1 : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() V12() ext-real ) Real) st 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) holds
ex s being ( ( ) ( V11() V12() ext-real ) Real) st
( 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS1 : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) holds
||.((f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS2 : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS2 : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS2 : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) ) ) ) );
end;

definition
let X be ( ( ) ( ) set ) ;
let RNS be ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) ;
let CNS be ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of CNS : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of RNS : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NCFCONT2:def 2
( X : ( ( ) ( ) CNORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of CNS : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() V12() ext-real ) Real) st 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) holds
ex s being ( ( ) ( V11() V12() ext-real ) Real) st
( 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) holds
||.((f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) ) ) ) );
end;

definition
let X be ( ( ) ( ) set ) ;
let RNS be ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) ;
let CNS be ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of RNS : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of CNS : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NCFCONT2:def 3
( X : ( ( ) ( ) CNORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of RNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() V12() ext-real ) Real) st 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) holds
ex s being ( ( ) ( V11() V12() ext-real ) Real) st
( 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) holds
||.((f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) ) ) ) );
end;

definition
let X be ( ( ) ( ) set ) ;
let CNS be ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of CNS : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NCFCONT2:def 4
( X : ( ( ) ( ) CNORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of CNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() V12() ext-real ) Real) st 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) holds
ex s being ( ( ) ( V11() V12() ext-real ) Real) st
( 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) holds
|.((f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ) .| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) ) ) ) );
end;

definition
let X be ( ( ) ( ) set ) ;
let CNS be ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of CNS : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NCFCONT2:def 5
( X : ( ( ) ( ) CNORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of CNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() V12() ext-real ) Real) st 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) holds
ex s being ( ( ) ( V11() V12() ext-real ) Real) st
( 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of CNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) holds
abs ((f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) ) ) ) );
end;

definition
let X be ( ( ) ( ) set ) ;
let RNS be ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of RNS : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NCFCONT2:def 6
( X : ( ( ) ( ) CNORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of RNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() V12() ext-real ) Real) st 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) holds
ex s being ( ( ) ( V11() V12() ext-real ) Real) st
( 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) CNORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( ) ( ) Element of X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() V12() ext-real ) Real) holds
|.((f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) CNORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) CNORMSTR ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) CNORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ) ) : ( ( ) ( V11() ) Element of COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) ) .| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() V12() ext-real ) Real) ) ) ) );
end;

theorem :: NCFCONT2:1
for X, X1 being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & X1 : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:2
for X, X1 being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & X1 : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:3
for X, X1 being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & X1 : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:4
for X, X1 being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) holds
f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:5
for X, X1 being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & f2 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) holds
f1 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:6
for X, X1 being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) holds
f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:7
for X, X1 being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) holds
f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:8
for X, X1 being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & f2 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) holds
f1 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:9
for X, X1 being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) & f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) holds
f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:10
for X being ( ( ) ( ) set )
for z being ( ( V11() ) ( V11() ) Complex)
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
z : ( ( V11() ) ( V11() ) Complex) (#) f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:11
for X being ( ( ) ( ) set )
for r being ( ( ) ( V11() V12() ext-real ) Real)
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
r : ( ( ) ( V11() V12() ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:12
for X being ( ( ) ( ) set )
for z being ( ( V11() ) ( V11() ) Complex)
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
z : ( ( V11() ) ( V11() ) Complex) (#) f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:13
for X being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
- f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:14
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
- f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:15
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
- f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:16
for X being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
||.f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .|| : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:17
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
||.f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .|| : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:18
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
||.f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .|| : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:19
for X being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:20
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:21
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:22
for X being ( ( ) ( ) set )
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:23
for X being ( ( ) ( ) set )
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:24
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined COMPLEX : ( ( ) ( non empty V47() V53() V54() ) set ) -valued Function-like complex-valued ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:25
for X being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_Lipschitzian_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:26
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_Lipschitzian_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:27
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_Lipschitzian_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:28
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_on Y : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) ;

theorem :: NCFCONT2:29
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_on Y : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) ;

theorem :: NCFCONT2:30
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_on Y : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) ;

theorem :: NCFCONT2:31
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is compact ;

theorem :: NCFCONT2:32
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is compact ;

theorem :: NCFCONT2:33
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is compact ;

theorem :: NCFCONT2:34
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V47() V48() V49() V50() V51() V52() V53() ) set ) & Y : ( ( ) ( ) Subset of ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) holds
ex x1, x2 being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st
( x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Y : ( ( ) ( ) Subset of ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in Y : ( ( ) ( ) Subset of ) & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = upper_bound (f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) ) : ( ( ) ( V47() V48() V49() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = lower_bound (f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) ) : ( ( ) ( V47() V48() V49() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ;

theorem :: NCFCONT2:35
for X being ( ( ) ( ) set )
for CNS1, CNS2 being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is constant holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:36
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is constant holds
f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NCFCONT2:37
for X being ( ( ) ( ) set )
for RNS being ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace)
for CNS being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is constant holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) ( non empty V107() V132() V133() V134() V135() V136() V137() V138() V142() V143() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

begin

definition
let M be ( ( non empty ) ( non empty ) CNORMSTR ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of M : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty ) ( non empty ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is contraction means :: NCFCONT2:def 7
 ex L being ( ( ) ( V11() V12() ext-real ) Real) st
( 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < L : ( ( ) ( V11() V12() ext-real ) Real) & L : ( ( ) ( V11() V12() ext-real ) Real) < 1 : ( ( ) ( non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) ) holds ||.((f : ( ( ) ( ) Element of M : ( ( ) ( ) CNORMSTR ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) - (f : ( ( ) ( ) Element of M : ( ( ) ( ) CNORMSTR ) ) . y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= L : ( ( ) ( V11() V12() ext-real ) Real) * ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) CNORMSTR ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) );
end;

registration
let M be ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) ;
cluster non empty Relation-like the carrier of M : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) CNORMSTR ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction for ( ( ) ( ) Element of K6(K7( the carrier of M : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) CNORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) CNORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) ;
mode Contraction of M is ( ( Function-like quasi_total contraction ) ( non empty Relation-like the carrier of M : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) CNORMSTR ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) CNORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

theorem :: NCFCONT2:38
for X being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) > 0 : ( ( ) ( empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) iff x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

theorem :: NCFCONT2:39
for X being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace)
for x, y being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) = ||.(y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like ) ComplexNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() V12() ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ;

theorem :: NCFCONT2:40
for X being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total contraction ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction ) Contraction of X : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) ) holds
ex xp being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st
( f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) ) = xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: NCFCONT2:41
for X being ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st ex n0 being ( ( ) ( V4() V5() V6() V10() V11() V12() ext-real V45() V46() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty V4() V5() V6() V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) st iter (f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,n0 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like ) set ) is ( ( Function-like quasi_total contraction ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction ) Contraction of X : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) ) holds
ex xp being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st
( f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) ) = xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ( non empty V107() V132() V133() V134() V142() V143() V148() V149() V150() V151() ComplexNormSpace-like V184() ) ComplexBanachSpace) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;