NFCONT

:: NFCONT_3 semantic presentation

begin

for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence)
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st rng seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( non empty V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) c= dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) holds
seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real V13() V14() V15() V16() V17() V18() ext-real non negative ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) in dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) ;

theorem :: NFCONT_3:2

theorem :: NFCONT_3:3

theorem :: NFCONT_3:4

theorem :: NFCONT_3:5

begin

definition

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;
let x0 be ( ( real ) ( V11() real ext-real ) number ) ;

pred f is_continuous_in x0 means :: NFCONT_3:def 1
( x0 : ( ( Function-like quasi_total ) ( Relation-like [:S : ( ( ) ( ) NORMSTR ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) -defined S : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of bool [:[:S : ( ( ) ( ) NORMSTR ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) in dom f : ( ( ) ( ) Element of S : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) & ( for s1 being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) st rng s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( non empty V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) c= dom f : ( ( ) ( ) Element of S : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) & s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) is convergent & lim s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) = x0 : ( ( Function-like quasi_total ) ( Relation-like [:S : ( ( ) ( ) NORMSTR ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) -defined S : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of bool [:[:S : ( ( ) ( ) NORMSTR ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) holds
( f : ( ( ) ( ) Element of S : ( ( ) ( ) NORMSTR ) ) /* s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of S : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) , the carrier of S : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is convergent & f : ( ( ) ( ) Element of S : ( ( ) ( ) NORMSTR ) ) /. x0 : ( ( Function-like quasi_total ) ( Relation-like [:S : ( ( ) ( ) NORMSTR ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) -defined S : ( ( ) ( ) NORMSTR ) -valued Function-like quasi_total ) Element of bool [:[:S : ( ( ) ( ) NORMSTR ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) ,S : ( ( ) ( ) NORMSTR ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) = lim (f : ( ( ) ( ) Element of S : ( ( ) ( ) NORMSTR ) ) /* s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of S : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) , the carrier of S : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of S : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) ) ) ) );

end;

theorem :: NFCONT_3:6

for X being ( ( ) ( ) set )
for x0 being ( ( real ) ( V11() real ext-real ) number )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st x0 : ( ( real ) ( V11() real ext-real ) number ) in X : ( ( ) ( ) set ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V11() real ext-real ) number ) holds
f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: NFCONT_3:7

theorem :: NFCONT_3:8

theorem :: NFCONT_3:9

theorem :: NFCONT_3:10

theorem :: NFCONT_3:11

theorem :: NFCONT_3:12

theorem :: NFCONT_3:13

for r being ( ( ) ( V11() real ext-real ) Real)
for x0 being ( ( real ) ( V11() real ext-real ) number )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is_continuous_in x0 : ( ( real ) ( V11() real ext-real ) number ) holds
r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is_continuous_in x0 : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: NFCONT_3:14

theorem :: NFCONT_3:15

definition

attr f is continuous means :: NFCONT_3:def 2
for x0 being ( ( real ) ( V11() real ext-real ) number ) st x0 : ( ( real ) ( V11() real ext-real ) number ) in dom f : ( ( ) ( ) Element of S : ( ( ) ( ) NORMSTR ) ) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( ) ( ) Element of S : ( ( ) ( ) NORMSTR ) ) is_continuous_in x0 : ( ( real ) ( V11() real ext-real ) number ) ;

end;

theorem :: NFCONT_3:16

theorem :: NFCONT_3:17

for X being ( ( ) ( ) set )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is continuous iff for x0 being ( ( real ) ( V11() real ext-real ) number )
for r being ( ( ) ( V11() real ext-real ) Real) st x0 : ( ( real ) ( V11() real ext-real ) number ) in X : ( ( ) ( ) set ) & 0 : ( ( ) ( empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V13() V14() V15() V16() V19() V57() ) set ) -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V11() real ext-real ) Real) holds
ex s being ( ( real ) ( V11() real ext-real ) number ) st
( 0 : ( ( ) ( empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V13() V14() V15() V16() V19() V57() ) set ) -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) ) < s : ( ( real ) ( V11() real ext-real ) number ) & ( for x1 being ( ( real ) ( V11() real ext-real ) number ) st x1 : ( ( real ) ( V11() real ext-real ) number ) in X : ( ( ) ( ) set ) & abs (x1 : ( ( real ) ( V11() real ext-real ) number ) - x0 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) < s : ( ( real ) ( V11() real ext-real ) number ) holds
||.((f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /. x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) - (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /. x0 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) < r : ( ( ) ( V11() real ext-real ) Real) ) ) ) ;

registration

cluster Function-like constant -> Function-like continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( ) ( ) NORMSTR ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

cluster Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;

cluster f : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

end;

theorem :: NFCONT_3:18

registration

cluster empty Function-like -> Function-like continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

cluster f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | X : ( ( trivial ) ( trivial ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( trivial ) ( trivial ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) set ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

end;

registration

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f1, f2 be ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) PartFunc of ,) ;

cluster f1 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) + f2 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

cluster f1 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) - f2 : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

end;

theorem :: NFCONT_3:19

theorem :: NFCONT_3:20

registration

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) PartFunc of ,) ;
let r be ( ( ) ( V11() real ext-real ) Real) ;

cluster r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) (#) f : ( ( Function-like continuous ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like continuous ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) -> Function-like continuous for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

end;

theorem :: NFCONT_3:21

for X being ( ( ) ( ) set )
for r being ( ( ) ( V11() real ext-real ) Real)
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is continuous holds
(r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: NFCONT_3:22

for X being ( ( ) ( ) set )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is continuous holds
( ||.f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .|| : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is continuous & (- f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is continuous ) ;

theorem :: NFCONT_3:23

theorem :: NFCONT_3:24

theorem :: NFCONT_3:25

begin

definition

attr f is Lipschitzian means :: NFCONT_3:def 3
ex r being ( ( real ) ( V11() real ext-real ) number ) st
( 0 : ( ( ) ( empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V13() V14() V15() V16() V19() V57() ) set ) -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V11() real ext-real ) number ) & ( for x1, x2 being ( ( real ) ( V11() real ext-real ) number ) st x1 : ( ( real ) ( V11() real ext-real ) number ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) & x2 : ( ( real ) ( V11() real ext-real ) number ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) holds
||.((f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) /. x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) - (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) /. x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) <= r : ( ( real ) ( V11() real ext-real ) number ) * (abs (x1 : ( ( real ) ( V11() real ext-real ) number ) - x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) ) );

end;

theorem :: NFCONT_3:26

for X being ( ( ) ( ) set )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian iff ex r being ( ( real ) ( V11() real ext-real ) number ) st
( 0 : ( ( ) ( empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V13() V14() V15() V16() V17() V18() V19() ext-real non positive non negative Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V13() V14() V15() V16() V19() V57() ) set ) -valued Function-like one-to-one constant functional complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V13() V14() V15() V16() V17() V18() V19() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( V11() real ext-real ) number ) & ( for x1, x2 being ( ( real ) ( V11() real ext-real ) number ) st x1 : ( ( real ) ( V11() real ext-real ) number ) in dom (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & x2 : ( ( real ) ( V11() real ext-real ) number ) in dom (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
||.((f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /. x1 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) - (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /. x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) <= r : ( ( real ) ( V11() real ext-real ) number ) * (abs (x1 : ( ( real ) ( V11() real ext-real ) number ) - x2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) ) ) ) ;

registration

cluster empty Function-like -> Function-like Lipschitzian for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

cluster empty Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;

cluster f : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

end;

theorem :: NFCONT_3:27

registration

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f1, f2 be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) PartFunc of ,) ;

cluster f1 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) + f2 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

cluster f1 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) - f2 : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

end;

theorem :: NFCONT_3:28

for X, X1 being ( ( ) ( ) set )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian holds
(f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) /\ b₂ : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

theorem :: NFCONT_3:29

for X, X1 being ( ( ) ( ) set )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f1, f2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X1 : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₂ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian holds
(f1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ X1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) /\ b₂ : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

registration

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) PartFunc of ,) ;
let p be ( ( ) ( V11() real ext-real ) Real) ;

cluster p : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ) (#) f : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ;

end;

theorem :: NFCONT_3:30

for X being ( ( ) ( ) set )
for p being ( ( ) ( V11() real ext-real ) Real)
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & X : ( ( ) ( ) set ) c= dom f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( V13() V14() V15() ) Element of bool REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) : ( ( ) ( ) set ) ) holds
(p : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₃ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ;

registration

let S be ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) PartFunc of ,) ;

cluster ||.f : ( ( Function-like Lipschitzian ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like Lipschitzian ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) .|| : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Function-like Lipschitzian for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;

end;

theorem :: NFCONT_3:31

for X being ( ( ) ( ) set )
for S being ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian holds
( - (f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & (- f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) is Lipschitzian & ||.f : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined the carrier of b₂ : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .|| : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -defined REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) ,REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is Lipschitzian ) ;

registration

cluster Function-like constant -> Function-like Lipschitzian for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

cluster Function-like Lipschitzian -> Function-like continuous for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V13() V14() V15() V19() V57() ) set ) , the carrier of S : ( ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) ( non empty V95() V120() V121() V122() V123() V124() V125() V126() V130() V131() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

end;

theorem :: NFCONT_3:32

theorem :: NFCONT_3:33