:: NFCONT_2 semantic presentation

begin

definition
let X be ( ( ) ( ) set ) ;
let S, T be ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of S : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NFCONT_2:def 1
( X : ( ( ) ( ) NORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of S : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() real ext-real ) Real) holds
ex s being ( ( ) ( V11() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() real ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) NORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) NORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() real ext-real ) Real) holds
||.((f : ( ( Function-like quasi_total ) ( Relation-like K7(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of T : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() real ext-real ) Real) ) ) ) );
end;

definition
let X be ( ( ) ( ) set ) ;
let S be ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like ) ( Relation-like the carrier of S : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) ;
pred f is_uniformly_continuous_on X means :: NFCONT_2:def 2
( X : ( ( ) ( ) NORMSTR ) c= dom f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) Element of K6( the carrier of S : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for r being ( ( ) ( V11() real ext-real ) Real) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() real ext-real ) Real) holds
ex s being ( ( ) ( V11() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V11() real ext-real ) Real) & ( for x1, x2 being ( ( ) ( ) Point of ( ( ) ( ) set ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) NORMSTR ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) NORMSTR ) & ||.(x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) Element of X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < s : ( ( ) ( V11() real ext-real ) Real) holds
abs ((f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) - (f : ( ( Function-like quasi_total ) ( Relation-like K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) -defined X : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of K6(K7(K7(X : ( ( ) ( ) NORMSTR ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < r : ( ( ) ( V11() real ext-real ) Real) ) ) ) );
end;

theorem :: NFCONT_2:1
for X, X1 being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X1 : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:2
for X, X1 being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:3
for X, X1 being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:4
for X being ( ( ) ( ) set )
for p being ( ( ) ( V11() real ext-real ) Real)
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
p : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b4 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:5
for X being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:6
for X being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .|| : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 :: NFCONT_2:7
for X being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:8
for X being ( ( ) ( ) set )
for S being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) is_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:9
for X being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

theorem :: NFCONT_2:10
for T, S being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on Y : ( ( ) ( ) Subset of ) ;

theorem :: NFCONT_2:11
for T, S being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is compact ;

theorem :: NFCONT_2:12
for S being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,)
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) <> {} : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & Y : ( ( ) ( ) Subset of ) is compact & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) /. x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) ) : ( ( ) ( V47() V48() V49() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) & f : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) /. x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() 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 ) PartFunc of ,) .: Y : ( ( ) ( ) Subset of ) ) : ( ( ) ( V47() V48() V49() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) ;

theorem :: NFCONT_2:13
for X being ( ( ) ( ) set )
for S, T being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K6(K7( the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is constant holds
f : ( ( Function-like ) ( Relation-like the carrier of b2 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_uniformly_continuous_on X : ( ( ) ( ) set ) ;

begin

definition
let M be ( ( non empty ) ( non empty ) NORMSTR ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of M : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is contraction means :: NFCONT_2:def 3
 ex L being ( ( ) ( V11() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < L : ( ( ) ( V11() real ext-real ) Real) & L : ( ( ) ( V11() real ext-real ) Real) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal 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 : ( ( ) ( ) NORMSTR ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) - (f : ( ( ) ( ) Element of M : ( ( ) ( ) NORMSTR ) ) . y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) <= L : ( ( ) ( V11() real ext-real ) Real) * ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of M : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) ) );
end;

registration
let M be ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) ;
cluster non empty Relation-like the carrier of M : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction for ( ( ) ( ) Element of K6(K7( the carrier of M : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of M : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;

definition
let M be ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) RealNormSpace) ;
mode Contraction of M is ( ( Function-like quasi_total contraction ) ( non empty Relation-like the carrier of M : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -defined the carrier of M : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

theorem :: NFCONT_2:14
for X being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction ) Contraction of X : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) ) 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: NFCONT_2:15
for X being ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st ex n0 being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,n0 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of K6(K7( the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is ( ( Function-like quasi_total contraction ) ( non empty Relation-like the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total contraction ) Contraction of X : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) ) 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( 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 V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) ( non empty V118() V143() V144() V145() V146() V147() V148() V149() V153() V154() RealNormSpace-like V187() ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
xp : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: NFCONT_2:16
for K, L, e being ( ( real ) ( V11() real ext-real ) number ) st 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < K : ( ( real ) ( V11() real ext-real ) number ) & K : ( ( real ) ( V11() real ext-real ) number ) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V45() V46() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) & 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V45() V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) < e : ( ( real ) ( V11() real ext-real ) number ) holds
ex n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) st abs (L : ( ( real ) ( V11() real ext-real ) number ) * (K : ( ( real ) ( V11() real ext-real ) number ) to_power n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V45() V46() V47() V48() V49() V50() V51() V52() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V47() V48() V49() V50() V51() V52() V53() ) Element of K6(REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( real ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V47() V48() V49() V53() V54() ) set ) ) < e : ( ( real ) ( V11() real ext-real ) number ) ;