for A, B, S, T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for f being ( ( Function-like V30( the U1 of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) )
for g being ( ( Function-like V30( the U1 of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30( the U1 of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st TopStruct(# the U1 of A : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of A : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( V1() ) Element of K6(K6( the U1 of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = TopStruct(# the U1 of B : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of B : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( V1() ) Element of K6(K6( the U1 of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) & TopStruct(# the U1 of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of S : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( V1() ) Element of K6(K6( the U1 of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) = TopStruct(# the U1 of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the topology of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( V1() ) Element of K6(K6( the U1 of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict TopSpace-like ) TopStruct ) & f : ( ( Function-like V30( the U1 of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) = g : ( ( Function-like V30( the U1 of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30( the U1 of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) & f : ( ( Function-like V30( the U1 of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₃ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is open holds
g : ( ( Function-like V30( the U1 of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) ( V16() Function-like V30( the U1 of b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) , the U1 of b₄ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is open ;

for m being ( ( natural ) ( natural V11() real ext-real ) Nat)
for P being ( ( ) ( ) Subset of ) holds
( P : ( ( ) ( ) Subset of ) is open iff for p being ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) st p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) in P : ( ( ) ( ) Subset of ) holds
ex r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st Ball (p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() open ) Element of K6( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= P : ( ( ) ( ) Subset of ) ) ;

for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for V being ( ( open ) ( open ) Subset of ) st p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) in V : ( ( open ) ( open ) Subset of ) holds
ex W being ( ( open ) ( open ) Subset of ) st
( f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) in W : ( ( open ) ( open ) Subset of ) & W : ( ( open ) ( open ) Subset of ) c= f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: V : ( ( open ) ( open ) Subset of ) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for V being ( ( open ) ( open ) Subset of )
for q being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) st q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) = f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) & p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) in V : ( ( open ) ( open ) Subset of ) holds
ex r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st Ball (q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: V : ( ( open ) ( open ) Subset of ) : ( ( ) ( ) Element of K6( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ex W being ( ( open ) ( open ) Subset of ) st
( f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) in W : ( ( open ) ( open ) Subset of ) & W : ( ( open ) ( open ) Subset of ) c= f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: (Ball (p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for M1, M2 being ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for q being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) = f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) holds
ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st Ball (q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: (Ball (p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( ) Element of K6( the U1 of b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

errorfrm ;

for m being ( ( natural ) ( natural V11() real ext-real ) Nat)
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ex W being ( ( open ) ( open ) Subset of ) st
( f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) in W : ( ( open ) ( open ) Subset of ) & W : ( ( open ) ( open ) Subset of ) c= f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: (Ball (p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( V1() open ) Element of K6( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for m, n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for f being ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st Ball ((f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V42(b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Element of the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ,s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() open ) Element of K6( the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: (Ball (p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( V1() open ) Element of K6( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) is open iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for V being ( ( open ) ( open ) Subset of ) st p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) in V : ( ( open ) ( open ) Subset of ) holds
ex r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st ].((f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) - r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ,((f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) + r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) .[ : ( ( ) ( V134() V135() V136() open ) Element of K6(REAL : ( ( ) ( V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) c= f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) .: V : ( ( open ) ( open ) Subset of ) : ( ( ) ( V134() V135() V136() ) Element of K6( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ex V being ( ( open ) ( open ) Subset of ) st
( f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) : ( ( ) ( ) Element of the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) in V : ( ( open ) ( open ) Subset of ) & V : ( ( open ) ( open ) Subset of ) c= f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) .: ].(p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) - r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ,(p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) + r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) .[ : ( ( ) ( V134() V135() V136() open ) Element of K6(REAL : ( ( ) ( V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for f being ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) is open iff for p being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st ].((f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) . p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) - s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ,((f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) . p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) + s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) .[ : ( ( ) ( V134() V135() V136() open ) Element of K6(REAL : ( ( ) ( V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) c= f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) .: ].(p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) - r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ,(p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) + r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) .[ : ( ( ) ( V134() V135() V136() open ) Element of K6(REAL : ( ( ) ( V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V134() V135() V136() ) Element of K6( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ;

for m being ( ( natural ) ( natural V11() real ext-real ) Nat)
for f being ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) is open iff for p being ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st ].((f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) . p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) - s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ,((f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) . p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) + s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) .[ : ( ( ) ( V134() V135() V136() open ) Element of K6(REAL : ( ( ) ( V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) c= f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) V124() V125() V126() ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() V134() V135() V136() ) set ) ) .: (Ball (p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( V1() open ) Element of K6( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V134() V135() V136() ) Element of K6( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ;

for m being ( ( natural ) ( natural V11() real ext-real ) Nat)
for f being ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) is open iff for p being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st Ball ((f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) ) : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Element of the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ,s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V1() open ) Element of K6( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= f : ( ( Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V189() ) TopStruct ) : ( ( ) ( V1() V134() V135() V136() ) set ) , the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() V134() V135() V136() ) set ) , ( ( ) ( V1() ) set ) ) .: ].(p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) - r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ,(p : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( V1() V134() V135() V136() ) set ) ) + r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( V11() real ext-real ) set ) .[ : ( ( ) ( V134() V135() V136() open ) Element of K6(REAL : ( ( ) ( V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is continuous iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for q being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) = f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) holds
ex W being ( ( open ) ( open ) Subset of ) st
( p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) in W : ( ( open ) ( open ) Subset of ) & f : ( ( Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: W : ( ( open ) ( open ) Subset of ) : ( ( ) ( ) Element of K6( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= Ball (q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is continuous iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for V being ( ( open ) ( open ) Subset of ) st f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) in V : ( ( open ) ( open ) Subset of ) holds
ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: (Ball (p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= V : ( ( open ) ( open ) Subset of ) ) ;

for M1, M2 being ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace)
for f being ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is continuous iff for p being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for q being ( ( ) ( ) Point of ( ( ) ( V1() ) set ) )
for r being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) = f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) holds
ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st f : ( ( Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TopSpaceMetr b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) , the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: (Ball (p : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( ) Element of K6( the U1 of b₁ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= Ball (q : ( ( ) ( ) Point of ( ( ) ( V1() ) set ) ) ,r : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) ) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty Reflexive discerning V83() triangle ) ( non empty Reflexive discerning V83() triangle Discerning ) MetrSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) ) ;

errorfrm ;

for m being ( ( natural ) ( natural V11() real ext-real ) Nat)
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) holds
( f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) is continuous iff for p being ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) )
for V being ( ( open ) ( open ) Subset of ) st f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) . p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) : ( ( ) ( ) Element of the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) in V : ( ( open ) ( open ) Subset of ) holds
ex s being ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) st f : ( ( Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) ( V16() Function-like V30( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) , the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) ) Function of ( ( ) ( V1() ) set ) , ( ( ) ( V1() ) set ) ) .: (Ball (p : ( ( ) ( V42(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) V43() V126() ) Point of ( ( ) ( V1() ) set ) ) ,s : ( ( real positive ) ( V1() V11() real ext-real positive non negative ) number ) )) : ( ( ) ( V1() open ) Element of K6( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V158() ) ( non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() V158() ) L15()) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6( the U1 of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( V1() ) set ) ) : ( ( ) ( ) set ) ) c= V : ( ( open ) ( open ) Subset of ) ) ;