begin
theorem
for
X,
Y being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
p0 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
D being ( ( non
empty ) ( non
empty )
Subset of )
for
E being ( ( non
empty ) ( non
empty )
Subset of )
for
f being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
D : ( ( non
empty ) ( non
empty )
Subset of )
` : ( ( ) ( )
Element of
K19( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
= {p0 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non
empty compact )
Element of
K19( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) &
E : ( ( non
empty ) ( non
empty )
Subset of )
` : ( ( ) ( )
Element of
K19( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
= {(f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . p0 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non
empty compact )
Element of
K19( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) &
X : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) is
T_2 &
Y : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) is
T_2 & ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. p : ( ( ) ( )
Subset of ) : ( ( ) ( )
set )
<> f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. p0 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) &
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
| D : ( ( non
empty ) ( non
empty )
Subset of ) : ( (
Function-like ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
K19(
K20( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) is ( (
Function-like quasi_total continuous ) (
Relation-like the
carrier of
(b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b5 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total continuous )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) & ( for
V being ( ( ) ( )
Subset of ) st
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. p0 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
in V : ( ( ) ( )
Subset of ) &
V : ( ( ) ( )
Subset of ) is
open holds
ex
W being ( ( ) ( )
Subset of ) st
(
p0 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
in W : ( ( ) ( )
Subset of ) &
W : ( ( ) ( )
Subset of ) is
open &
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
.: W : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K19( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
c= V : ( ( ) ( )
Subset of ) ) ) holds
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous ;
begin
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous & ( for
q being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. q : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
<> 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
ex
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
( ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( (
real ) (
V28()
real ext-real )
number ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number ) holds
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= (r1 : ( ( real ) ( V28() real ext-real ) number ) / r2 : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) (
V28()
real ext-real )
set )
^2 : ( ( ) (
V28()
real ext-real )
set ) ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous ) ;
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous & ( for
q being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. q : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
<> 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
ex
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
( ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( (
real ) (
V28()
real ext-real )
number ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number ) holds
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) )
+ ((r1 : ( ( real ) ( V28() real ext-real ) number ) / r2 : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( V28() real ext-real ) set ) ^2) : ( ( ) (
V28()
real ext-real )
set ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous ) ;
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous & ( for
q being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. q : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
<> 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
ex
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
( ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( (
real ) (
V28()
real ext-real )
number ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number ) holds
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= sqrt (1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) + ((r1 : ( ( real ) ( V28() real ext-real ) number ) / r2 : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( V28() real ext-real ) set ) ^2) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous ) ;
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous & ( for
q being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. q : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
<> 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
ex
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
( ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( (
real ) (
V28()
real ext-real )
number ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number ) holds
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number )
/ (sqrt (1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) + ((r1 : ( ( real ) ( V28() real ext-real ) number ) / r2 : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( V28() real ext-real ) set ) ^2) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous ) ;
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous & ( for
q being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. q : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
<> 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
ex
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
( ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( (
real ) (
V28()
real ext-real )
number ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number ) holds
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number )
/ (sqrt (1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) + ((r1 : ( ( real ) ( V28() real ext-real ) number ) / r2 : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( V28() real ext-real ) set ) ^2) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous ) ;
begin
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous & ( for
q being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. q : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
<> 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
ex
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
( ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( (
real ) (
V28()
real ext-real )
number ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number ) holds
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number )
* (sqrt (1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) + ((r1 : ( ( real ) ( V28() real ext-real ) number ) / r2 : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( V28() real ext-real ) set ) ^2) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous ) ;
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous & ( for
q being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. q : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
<> 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) ) holds
ex
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
( ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
r1,
r2 being ( (
real ) (
V28()
real ext-real )
number ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r1 : ( (
real ) (
V28()
real ext-real )
number ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number ) holds
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= r2 : ( (
real ) (
V28()
real ext-real )
number )
* (sqrt (1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) + ((r1 : ( ( real ) ( V28() real ext-real ) number ) / r2 : ( ( real ) ( V28() real ext-real ) number ) ) : ( ( ) ( V28() real ext-real ) set ) ^2) : ( ( ) ( V28() real ext-real ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) is
continuous ) ;
theorem
for
f,
g being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) )
for
C0,
KXP,
KXN,
KYP,
KYN being ( ( ) (
functional )
Subset of )
for
O,
I being ( ( ) (
V28()
real ext-real )
Point of ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) st
O : ( ( ) (
V28()
real ext-real )
Point of ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) &
I : ( ( ) (
V28()
real ext-real )
Point of ( ( ) ( non
empty V162()
V163()
V164() )
set ) )
= 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) &
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) is
continuous &
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) is
one-to-one &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) is
continuous &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) is
one-to-one &
C0 : ( ( ) (
functional )
Subset of )
= { p : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) where p is ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) : |.p : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) .| : ( ( ) ( V28() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) <= 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) } &
KXP : ( ( ) (
functional )
Subset of )
= { q1 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) where q1 is ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) : ( |.q1 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) .| : ( ( ) ( V28() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) = 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) & q1 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) <= q1 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) & q1 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) >= - (q1 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) } &
KXN : ( ( ) (
functional )
Subset of )
= { q2 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) where q2 is ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) : ( |.q2 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) .| : ( ( ) ( V28() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) = 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) & q2 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) >= q2 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) & q2 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) <= - (q2 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) } &
KYP : ( ( ) (
functional )
Subset of )
= { q3 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) where q3 is ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) : ( |.q3 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) .| : ( ( ) ( V28() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) = 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) & q3 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) >= q3 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) & q3 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) >= - (q3 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) } &
KYN : ( ( ) (
functional )
Subset of )
= { q4 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) where q4 is ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) : ( |.q4 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) .| : ( ( ) ( V28() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) = 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) & q4 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) <= q4 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) & q4 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `2 : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) <= - (q4 : ( ( ) ( Relation-like Function-like V43(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) V111() V154() ) Point of ( ( ) ( functional non empty ) set ) ) `1) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( V28() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) ) } &
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) )
. O : ( ( ) (
V28()
real ext-real )
Point of ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
Relation-like Function-like V43(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) )
in KXN : ( ( ) (
functional )
Subset of ) &
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) )
. I : ( ( ) (
V28()
real ext-real )
Point of ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
Relation-like Function-like V43(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) )
in KXP : ( ( ) (
functional )
Subset of ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) )
. O : ( ( ) (
V28()
real ext-real )
Point of ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
Relation-like Function-like V43(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) )
in KYN : ( ( ) (
functional )
Subset of ) &
g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) )
. I : ( ( ) (
V28()
real ext-real )
Point of ( ( ) ( non
empty V162()
V163()
V164() )
set ) ) : ( ( ) (
Relation-like Function-like V43(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K19(
REAL : ( ( ) ( non
empty V36()
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) )
in KYP : ( ( ) (
functional )
Subset of ) &
rng f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) )
c= C0 : ( ( ) (
functional )
Subset of ) &
rng g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) )
c= C0 : ( ( ) (
functional )
Subset of ) holds
rng f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) )
meets rng g : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V110() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V110() )
TopStruct ) ) : ( ( ) ( non
empty V162()
V163()
V164() )
set )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V162()
V163()
V164() )
set ) , ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K19(REAL : ( ( ) ( non empty V36() V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) ;