REAL is non empty V36() V168() V169() V170() V174() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V36() V168() V174() set
omega is non empty epsilon-transitive epsilon-connected ordinal V168() V169() V170() V171() V172() V173() V174() set
K6(omega) is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
INT is non empty V36() V168() V169() V170() V171() V172() V174() set
K7(1,1) is RAT -valued INT -valued V158() V159() V160() V161() set
RAT is non empty V36() V168() V169() V170() V171() V174() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is RAT -valued INT -valued V158() V159() V160() V161() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is V158() V159() V160() set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is V158() V159() V160() set
K7(K7(REAL,REAL),REAL) is V158() V159() V160() set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
K7(2,2) is RAT -valued INT -valued V158() V159() V160() V161() set
K7(K7(2,2),REAL) is V158() V159() V160() set
K6(K7(K7(2,2),REAL)) is set
K272() is V116() TopStruct
the carrier of K272() is V168() V169() V170() set
RealSpace is non empty strict Reflexive discerning V86() triangle Discerning V116() MetrStruct
R^1 is non empty strict TopSpace-like V116() TopStruct
K6(NAT) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() L15()
the carrier of (TOP-REAL 2) is non empty set
K6( the carrier of (TOP-REAL 2)) is set
K7( the carrier of (TOP-REAL 2),REAL) is V158() V159() V160() set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
K7(COMPLEX,COMPLEX) is V158() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is V158() V159() V160() set
K6(K7(COMPLEX,REAL)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V158() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(RAT,RAT) is RAT -valued V158() V159() V160() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is RAT -valued V158() V159() V160() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is RAT -valued INT -valued V158() V159() V160() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is RAT -valued INT -valued V158() V159() V160() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is RAT -valued INT -valued V158() V159() V160() V161() set
K7(K7(NAT,NAT),NAT) is RAT -valued INT -valued V158() V159() V160() V161() set
K6(K7(K7(NAT,NAT),NAT)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V168() V169() V170() V171() V172() V173() V174() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V120() V121() V168() V169() V170() V171() V172() V173() V174() Element of NAT
TopSpaceMetr RealSpace is non empty strict TopSpace-like TopStruct
the carrier of R^1 is non empty V168() V169() V170() set
Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V116() SubSpace of R^1
real_dist is Relation-like K7(REAL,REAL) -defined REAL -valued Function-like V33(K7(REAL,REAL), REAL ) V158() V159() V160() Element of K6(K7(K7(REAL,REAL),REAL))
MetrStruct(# REAL,real_dist #) is strict MetrStruct
K7(NAT,REAL) is V158() V159() V160() set
K6(K7(NAT,REAL)) is set
K6( the carrier of R^1) is set
[.0,1.] is V168() V169() V170() Element of K6(REAL)
I[01] is TopSpace-like V116() SubSpace of R^1
the carrier of I[01] is V168() V169() V170() set
P is non empty Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of P is non empty set
K7(NAT, the carrier of P) is set
K6(K7(NAT, the carrier of P)) is set
TopSpaceMetr P is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr P) is non empty set
K6( the carrier of (TopSpaceMetr P)) is set
P1 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))
lim P1 is Element of the carrier of P
U2 is Element of K6( the carrier of (TopSpaceMetr P))
U3 is Element of K6( the carrier of (TopSpaceMetr P))
f is V11() real ext-real set
Ball ((lim P1),f) is Element of K6( the carrier of P)
K6( the carrier of P) is set
r2 is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
P1 . r1 is Element of the carrier of P
dist ((P1 . r1),(lim P1)) is V11() real ext-real Element of REAL
U2 /\ U3 is Element of K6( the carrier of (TopSpaceMetr P))
U3 is Element of K6( the carrier of (TopSpaceMetr P))
Cl U3 is Element of K6( the carrier of (TopSpaceMetr P))
P is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr P is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr P) is non empty set
P1 is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr P1 is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr P1) is non empty set
K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) is set
K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1))) is set
the carrier of P is non empty set
K7(NAT, the carrier of P) is set
K6(K7(NAT, the carrier of P)) is set
the carrier of P1 is non empty set
K7(NAT, the carrier of P1) is set
K6(K7(NAT, the carrier of P1)) is set
U2 is Relation-like the carrier of (TopSpaceMetr P) -defined the carrier of (TopSpaceMetr P1) -valued Function-like V33( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) Element of K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)))
U3 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))
U2 * U3 is Relation-like NAT -defined the carrier of (TopSpaceMetr P1) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P1)))
K7(NAT, the carrier of (TopSpaceMetr P1)) is set
K6(K7(NAT, the carrier of (TopSpaceMetr P1))) is set
dom U2 is Element of K6( the carrier of (TopSpaceMetr P))
K6( the carrier of (TopSpaceMetr P)) is set
dom U3 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
rng U3 is Element of K6( the carrier of P)
K6( the carrier of P) is set
dom (U2 * U3) is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
P is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr P is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr P) is non empty set
P1 is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr P1 is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr P1) is non empty set
K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) is set
K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1))) is set
the carrier of P is non empty set
K7(NAT, the carrier of P) is set
K6(K7(NAT, the carrier of P)) is set
the carrier of P1 is non empty set
K7(NAT, the carrier of P1) is set
K6(K7(NAT, the carrier of P1)) is set
U2 is Relation-like the carrier of (TopSpaceMetr P) -defined the carrier of (TopSpaceMetr P1) -valued Function-like V33( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)) Element of K6(K7( the carrier of (TopSpaceMetr P), the carrier of (TopSpaceMetr P1)))
U3 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))
U2 * U3 is Relation-like NAT -defined the carrier of (TopSpaceMetr P1) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P1)))
K7(NAT, the carrier of (TopSpaceMetr P1)) is set
K6(K7(NAT, the carrier of (TopSpaceMetr P1))) is set
f is Relation-like NAT -defined the carrier of P1 -valued Function-like V33( NAT , the carrier of P1) Element of K6(K7(NAT, the carrier of P1))
lim U3 is Element of the carrier of P
dom U2 is Element of K6( the carrier of (TopSpaceMetr P))
K6( the carrier of (TopSpaceMetr P)) is set
U2 . (lim U3) is set
rng U2 is Element of K6( the carrier of (TopSpaceMetr P1))
K6( the carrier of (TopSpaceMetr P1)) is set
Q is Element of the carrier of P1
g is V11() real ext-real Element of REAL
Ball (Q,g) is Element of K6( the carrier of P1)
K6( the carrier of P1) is set
r0 is Element of K6( the carrier of (TopSpaceMetr P1))
r1 is Element of the carrier of (TopSpaceMetr P)
t1 is Element of K6( the carrier of (TopSpaceMetr P))
U2 .: t1 is Element of K6( the carrier of (TopSpaceMetr P1))
S2 is V11() real ext-real set
Ball ((lim U3),S2) is Element of K6( the carrier of P)
K6( the carrier of P) is set
R2 is V11() real ext-real Element of REAL
s2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
S1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . S1 is Element of the carrier of P1
dist ((f . S1),Q) is V11() real ext-real Element of REAL
U3 . S1 is Element of the carrier of P
dist ((U3 . S1),(lim U3)) is V11() real ext-real Element of REAL
U2 . (U3 . S1) is set
dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
the carrier of RealSpace is non empty V168() V169() V170() set
K7(NAT, the carrier of RealSpace) is V158() V159() V160() set
K6(K7(NAT, the carrier of RealSpace)) is set
P is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
lim P is V11() real ext-real Element of REAL
P1 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))
lim P1 is V11() real ext-real Element of the carrier of RealSpace
U2 is V11() real ext-real set
f is V11() real ext-real Element of the carrier of RealSpace
r2 is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
P1 . Q is V11() real ext-real Element of the carrier of RealSpace
dist ((P1 . Q),f) is V11() real ext-real Element of REAL
P . Q is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
real_dist . (g,U2) is set
U3 is V11() real ext-real Element of REAL
g - U3 is V11() real ext-real Element of REAL
abs (g - U3) is V11() real ext-real Element of REAL
U2 is V11() real ext-real Element of the carrier of RealSpace
U3 is V11() real ext-real Element of REAL
f is V11() real ext-real set
r2 is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
P . Q is V11() real ext-real Element of REAL
(P . Q) - U3 is V11() real ext-real Element of REAL
abs ((P . Q) - U3) is V11() real ext-real Element of REAL
P1 . Q is V11() real ext-real Element of the carrier of RealSpace
dist ((P1 . Q),U2) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
real_dist . (g,U3) is V11() real ext-real Element of REAL
g - U3 is V11() real ext-real Element of REAL
abs (g - U3) is V11() real ext-real Element of REAL
U2 is V11() real ext-real Element of REAL
U3 is V11() real ext-real set
f is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
P . r1 is V11() real ext-real Element of REAL
(P . r1) - U2 is V11() real ext-real Element of REAL
abs ((P . r1) - U2) is V11() real ext-real Element of REAL
P1 . r1 is V11() real ext-real Element of the carrier of RealSpace
dist ((P1 . r1),(lim P1)) is V11() real ext-real Element of REAL
real_dist . ((P . r1),U2) is V11() real ext-real Element of REAL
P is V11() real ext-real set
P1 is V11() real ext-real set
[.P,P1.] is V168() V169() V170() Element of K6(REAL)
Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set
K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set
K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
rng U2 is V168() V169() V170() Element of K6(REAL)
U2 . 0 is V11() real ext-real Element of REAL
dom U2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
U3 is V11() real ext-real Element of REAL
P is V11() real ext-real set
P1 is V11() real ext-real set
Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set
K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set
K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set
U2 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))
[.P,P1.] is V168() V169() V170() Element of K6(REAL)
dom U2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
rng U2 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))
K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set
P is V11() real ext-real set
P1 is V11() real ext-real set
Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set
K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set
K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set
U2 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))
lim U2 is Element of the carrier of (Closed-Interval-MSpace (P,P1))
U3 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))
lim U3 is V11() real ext-real Element of the carrier of RealSpace
[.P,P1.] is V168() V169() V170() Element of K6(REAL)
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . r2 is V11() real ext-real Element of the carrier of RealSpace
dom U2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
U2 . r2 is Element of the carrier of (Closed-Interval-MSpace (P,P1))
rng U2 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))
K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set
f is V168() V169() V170() Element of K6( the carrier of R^1)
r2 is V11() real ext-real Element of the carrier of RealSpace
r1 is Element of the carrier of (Closed-Interval-MSpace (P,P1))
Q is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . r0 is Element of the carrier of (Closed-Interval-MSpace (P,P1))
dist ((U2 . r0),r1) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (P,P1)) is Relation-like K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) -defined REAL -valued Function-like V33(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL))
K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) is set
K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL) is V158() V159() V160() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL)) is set
the distance of (Closed-Interval-MSpace (P,P1)) . ((U2 . r0),r1) is V11() real ext-real Element of REAL
the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V33(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))
K7( the carrier of RealSpace, the carrier of RealSpace) is V158() V159() V160() set
K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is V158() V159() V160() set
K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set
the distance of RealSpace . ((U2 . r0),r1) is set
U3 . r0 is V11() real ext-real Element of the carrier of RealSpace
dist ((U3 . r0),r2) is V11() real ext-real Element of REAL
r2 is Element of the carrier of (Closed-Interval-MSpace (P,P1))
r1 is V11() real ext-real Element of the carrier of RealSpace
Q is V11() real ext-real Element of REAL
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . r0 is V11() real ext-real Element of the carrier of RealSpace
dist ((U3 . r0),r1) is V11() real ext-real Element of REAL
U2 . r0 is Element of the carrier of (Closed-Interval-MSpace (P,P1))
dist ((U2 . r0),r2) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (P,P1)) is Relation-like K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) -defined REAL -valued Function-like V33(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL))
K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) is set
K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL) is V158() V159() V160() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL)) is set
the distance of (Closed-Interval-MSpace (P,P1)) . ((U2 . r0),r2) is V11() real ext-real Element of REAL
the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V33(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))
K7( the carrier of RealSpace, the carrier of RealSpace) is V158() V159() V160() set
K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is V158() V159() V160() set
K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set
the distance of RealSpace . ((U2 . r0),r2) is set
r2 is V11() real ext-real Element of the carrier of RealSpace
r1 is V11() real ext-real Element of REAL
Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . g is V11() real ext-real Element of the carrier of RealSpace
dist ((U3 . g),r2) is V11() real ext-real Element of REAL
U2 . g is Element of the carrier of (Closed-Interval-MSpace (P,P1))
dist ((U2 . g),(lim U2)) is V11() real ext-real Element of REAL
the distance of (Closed-Interval-MSpace (P,P1)) is Relation-like K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) -defined REAL -valued Function-like V33(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL))
K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))) is set
K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL) is V158() V159() V160() set
K6(K7(K7( the carrier of (Closed-Interval-MSpace (P,P1)), the carrier of (Closed-Interval-MSpace (P,P1))),REAL)) is set
the distance of (Closed-Interval-MSpace (P,P1)) . ((U2 . g),(lim U2)) is V11() real ext-real Element of REAL
the distance of RealSpace is Relation-like K7( the carrier of RealSpace, the carrier of RealSpace) -defined REAL -valued Function-like V33(K7( the carrier of RealSpace, the carrier of RealSpace), REAL ) V158() V159() V160() Element of K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL))
K7( the carrier of RealSpace, the carrier of RealSpace) is V158() V159() V160() set
K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL) is V158() V159() V160() set
K6(K7(K7( the carrier of RealSpace, the carrier of RealSpace),REAL)) is set
the distance of RealSpace . ((U2 . g),(lim U2)) is set
P is V11() real ext-real set
P1 is V11() real ext-real set
Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set
K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set
K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
lim U2 is V11() real ext-real Element of REAL
U3 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))
lim U3 is Element of the carrier of (Closed-Interval-MSpace (P,P1))
f is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))
lim f is V11() real ext-real Element of the carrier of RealSpace
P is V11() real ext-real set
P1 is V11() real ext-real set
Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set
K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set
K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
U3 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))
P1 + 1 is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . f is V11() real ext-real Element of REAL
dom U3 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
rng U3 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))
K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set
[.P,P1.] is V168() V169() V170() Element of K6(REAL)
P is V11() real ext-real set
P1 is V11() real ext-real set
Closed-Interval-MSpace (P,P1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (P,P1)) is non empty set
K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))) is set
K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1)))) is set
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
U3 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (P,P1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (P,P1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (P,P1))))
P - 1 is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . f is V11() real ext-real Element of REAL
P + 1 is V11() real ext-real Element of REAL
dom U3 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
rng U3 is Element of K6( the carrier of (Closed-Interval-MSpace (P,P1)))
K6( the carrier of (Closed-Interval-MSpace (P,P1))) is set
[.P,P1.] is V168() V169() V170() Element of K6(REAL)
P is non empty V168() V169() V170() Element of K6(REAL)
upper_bound P is V11() real ext-real Element of REAL
P1 is V11() real ext-real set
U2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
1 / (U2 + 1) is V11() real ext-real non negative Element of REAL
P1 - (1 / (U2 + 1)) is V11() real ext-real set
(U2 + 1) " is non empty V11() real ext-real positive non negative Element of REAL
U3 is V11() real ext-real set
f is V11() real ext-real set
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
U3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f is set
U3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . (U3 + 1) is V11() real ext-real Element of REAL
r1 is V11() real ext-real set
r2 is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . (r0 + 1) is V11() real ext-real Element of REAL
r1 is V11() real ext-real set
r2 is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . (r0 + 1) is V11() real ext-real Element of REAL
r1 is V11() real ext-real set
r2 is V11() real ext-real set
r1 is V11() real ext-real set
r2 is V11() real ext-real set
Q is set
g is set
r2 is set
r1 is set
U2 . 0 is V11() real ext-real Element of REAL
U3 is Relation-like Function-like set
dom U3 is set
U3 . 0 is set
U3 is Relation-like Function-like set
dom U3 is set
U3 . 0 is set
rng U3 is set
f is set
r2 is set
U3 . r2 is set
Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . Q is set
Q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . (Q + 1) is set
U2 . (Q + 1) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . r1 is set
f is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . r2 is V11() real ext-real Element of REAL
f . r2 is V11() real ext-real Element of REAL
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . (r2 + 1) is V11() real ext-real Element of REAL
f . (r2 + 1) is V11() real ext-real Element of REAL
U3 . r2 is set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
f . 0 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r2 + 1) is V11() real ext-real Element of REAL
U2 . (r2 + 1) is V11() real ext-real Element of REAL
dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
U3 . r2 is set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r2 + 1) is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r2 + 1) is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r1 is V11() real ext-real Element of REAL
r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r1 + 1) is V11() real ext-real Element of REAL
U2 . (r1 + 1) is V11() real ext-real Element of REAL
U3 . r1 is set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r1 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
f . r1 is V11() real ext-real Element of REAL
rng f is V168() V169() V170() Element of K6(REAL)
r2 is set
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r1 is V11() real ext-real Element of REAL
r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r1 + 1) is V11() real ext-real Element of REAL
U2 . (r1 + 1) is V11() real ext-real Element of REAL
U3 . r1 is set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
U3 . (r1 + 1) is set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
r1 is set
f . r1 is V11() real ext-real Element of REAL
(upper_bound P) + 1 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
lim f is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
(upper_bound P) - r2 is V11() real ext-real Element of REAL
1 / r2 is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
(r1 + 1) * r2 is V11() real ext-real Element of REAL
(1 / r2) * r2 is V11() real ext-real Element of REAL
((r1 + 1) * r2) / (r1 + 1) is V11() real ext-real Element of REAL
1 / (r1 + 1) is V11() real ext-real non negative Element of REAL
P1 - (1 / (r1 + 1)) is V11() real ext-real Element of REAL
P1 - r2 is V11() real ext-real Element of REAL
U2 . r1 is V11() real ext-real Element of REAL
f . r1 is V11() real ext-real Element of REAL
(upper_bound P) - (lim f) is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
(upper_bound P) - r2 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
P is non empty V168() V169() V170() Element of K6(REAL)
lower_bound P is V11() real ext-real Element of REAL
P1 is V11() real ext-real set
U2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
1 / (U2 + 1) is V11() real ext-real non negative Element of REAL
P1 + (1 / (U2 + 1)) is V11() real ext-real set
(U2 + 1) " is non empty V11() real ext-real positive non negative Element of REAL
U3 is V11() real ext-real set
f is V11() real ext-real set
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
U2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
U3 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f is set
U3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . (U3 + 1) is V11() real ext-real Element of REAL
r2 is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . (r0 + 1) is V11() real ext-real Element of REAL
r2 is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U2 . (r0 + 1) is V11() real ext-real Element of REAL
r2 is V11() real ext-real set
r1 is V11() real ext-real set
r2 is V11() real ext-real set
r1 is V11() real ext-real set
Q is set
g is set
r2 is set
r1 is set
U2 . 0 is V11() real ext-real Element of REAL
U3 is Relation-like Function-like set
dom U3 is set
U3 . 0 is set
U3 is Relation-like Function-like set
dom U3 is set
U3 . 0 is set
rng U3 is set
f is set
r2 is set
U3 . r2 is set
Q is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . Q is set
Q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . (Q + 1) is set
U2 . (Q + 1) is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r0 is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
U3 . r1 is set
f is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
U2 . r2 is V11() real ext-real Element of REAL
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r2 + 1) is V11() real ext-real Element of REAL
U2 . (r2 + 1) is V11() real ext-real Element of REAL
U3 . r2 is set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
f . 0 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r2 + 1) is V11() real ext-real Element of REAL
f . r2 is V11() real ext-real Element of REAL
U2 . (r2 + 1) is V11() real ext-real Element of REAL
dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
U3 . r2 is set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
Q is V11() real ext-real set
r1 is V11() real ext-real set
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r2 + 1) is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
r2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r2 + 1) is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r1 is V11() real ext-real Element of REAL
r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r1 + 1) is V11() real ext-real Element of REAL
U2 . (r1 + 1) is V11() real ext-real Element of REAL
U3 . r1 is set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
dom f is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r1 is V11() real ext-real Element of REAL
f . r2 is V11() real ext-real Element of REAL
rng f is V168() V169() V170() Element of K6(REAL)
r2 is set
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r1 is V11() real ext-real Element of REAL
r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . (r1 + 1) is V11() real ext-real Element of REAL
U2 . (r1 + 1) is V11() real ext-real Element of REAL
U3 . r1 is set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
U3 . (r1 + 1) is set
g is V11() real ext-real set
Q is V11() real ext-real set
g is V11() real ext-real set
Q is V11() real ext-real set
r1 is set
f . r1 is V11() real ext-real Element of REAL
(lower_bound P) - 1 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
(lower_bound P) + 1 is V11() real ext-real Element of REAL
lim f is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
(lower_bound P) + r2 is V11() real ext-real Element of REAL
1 / r2 is V11() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
(r1 + 1) * r2 is V11() real ext-real Element of REAL
(1 / r2) * r2 is V11() real ext-real Element of REAL
((r1 + 1) * r2) / (r1 + 1) is V11() real ext-real Element of REAL
1 / (r1 + 1) is V11() real ext-real non negative Element of REAL
P1 + r2 is V11() real ext-real Element of REAL
P1 + (1 / (r1 + 1)) is V11() real ext-real Element of REAL
U2 . r1 is V11() real ext-real Element of REAL
f . r1 is V11() real ext-real Element of REAL
(lim f) - (lower_bound P) is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
- (lower_bound P) is V11() real ext-real Element of REAL
(lim f) + (- (lower_bound P)) is V11() real ext-real Element of REAL
(lower_bound P) + ((lim f) + (- (lower_bound P))) is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
f . r2 is V11() real ext-real Element of REAL
(lower_bound P) + 1 is V11() real ext-real Element of REAL
P is non empty Reflexive discerning V86() triangle Discerning MetrStruct
TopSpaceMetr P is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr P) is non empty set
K7( the carrier of I[01], the carrier of (TopSpaceMetr P)) is set
K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr P))) is set
K6( the carrier of (TopSpaceMetr P)) is set
the carrier of P is non empty set
P1 is Relation-like the carrier of I[01] -defined the carrier of (TopSpaceMetr P) -valued Function-like V33( the carrier of I[01], the carrier of (TopSpaceMetr P)) Element of K6(K7( the carrier of I[01], the carrier of (TopSpaceMetr P)))
U2 is Element of K6( the carrier of (TopSpaceMetr P))
U3 is Element of K6( the carrier of (TopSpaceMetr P))
U2 \/ U3 is Element of K6( the carrier of (TopSpaceMetr P))
U2 /\ U3 is Element of K6( the carrier of (TopSpaceMetr P))
f is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
P1 . f is set
P1 . r2 is set
{ b1 where b1 is V11() real ext-real Element of REAL : ( f <= b1 & b1 <= r2 & P1 . b1 in U2 ) } is set
r1 is set
Q is V11() real ext-real Element of REAL
P1 . Q is set
r1 is non empty V168() V169() V170() Element of K6(REAL)
Q is V11() real ext-real set
g is V11() real ext-real Element of REAL
P1 . g is set
Q is ext-real set
g is V11() real ext-real Element of REAL
P1 . g is set
upper_bound r1 is V11() real ext-real Element of REAL
Q is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
rng Q is V168() V169() V170() Element of K6(REAL)
lim Q is V11() real ext-real Element of REAL
g is set
r0 is V11() real ext-real Element of REAL
P1 . r0 is set
Closed-Interval-MSpace (0,1) is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of RealSpace
the carrier of (Closed-Interval-MSpace (0,1)) is non empty set
K7(NAT, the carrier of (Closed-Interval-MSpace (0,1))) is set
K6(K7(NAT, the carrier of (Closed-Interval-MSpace (0,1)))) is set
TopSpaceMetr (Closed-Interval-MSpace (0,1)) is non empty strict TopSpace-like TopStruct
K7(NAT, the carrier of P) is set
K6(K7(NAT, the carrier of P)) is set
g is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (0,1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (0,1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (0,1))))
P1 * g is Relation-like NAT -defined the carrier of (TopSpaceMetr P) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P)))
K7(NAT, the carrier of (TopSpaceMetr P)) is set
K6(K7(NAT, the carrier of (TopSpaceMetr P))) is set
r0 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))
dom P1 is V168() V169() V170() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
lim g is Element of the carrier of (Closed-Interval-MSpace (0,1))
P1 . (lim g) is set
rng P1 is Element of K6( the carrier of (TopSpaceMetr P))
S2 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))
lim S2 is V11() real ext-real Element of the carrier of RealSpace
t1 is Element of the carrier of P
R2 is V11() real ext-real Element of REAL
s2 is V11() real ext-real Element of REAL
S1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
S2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r0 . S2 is Element of the carrier of P
dist ((r0 . S2),t1) is V11() real ext-real Element of REAL
dom r0 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
g . S2 is Element of the carrier of (Closed-Interval-MSpace (0,1))
P1 . (g . S2) is set
dist ((lim g),(g . S2)) is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( upper_bound r1 <= b1 & b1 <= r2 & P1 . b1 in U3 ) } is set
R2 is set
s2 is V11() real ext-real Element of REAL
P1 . s2 is set
R2 is non empty V168() V169() V170() Element of K6(REAL)
s2 is V11() real ext-real set
S1 is V11() real ext-real Element of REAL
P1 . S1 is set
s2 is ext-real set
S1 is V11() real ext-real Element of REAL
P1 . S1 is set
lower_bound R2 is V11() real ext-real Element of REAL
s2 is Relation-like NAT -defined REAL -valued Function-like V33( NAT , REAL ) V158() V159() V160() Element of K6(K7(NAT,REAL))
rng s2 is V168() V169() V170() Element of K6(REAL)
lim s2 is V11() real ext-real Element of REAL
S1 is set
S2 is V11() real ext-real Element of REAL
P1 . S2 is set
S1 is Relation-like NAT -defined the carrier of (Closed-Interval-MSpace (0,1)) -valued Function-like V33( NAT , the carrier of (Closed-Interval-MSpace (0,1))) Element of K6(K7(NAT, the carrier of (Closed-Interval-MSpace (0,1))))
S2 is Relation-like NAT -defined the carrier of RealSpace -valued Function-like V33( NAT , the carrier of RealSpace) V158() V159() V160() Element of K6(K7(NAT, the carrier of RealSpace))
lim S2 is V11() real ext-real Element of the carrier of RealSpace
lim S1 is Element of the carrier of (Closed-Interval-MSpace (0,1))
S00 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
r0 . S00 is Element of the carrier of P
dom Q is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
Q . S00 is V11() real ext-real Element of REAL
dom r0 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
t1 is V11() real ext-real Element of REAL
P1 . t1 is set
lim r0 is Element of the carrier of P
P1 . (lim Q) is set
P1 * S1 is Relation-like NAT -defined the carrier of (TopSpaceMetr P) -valued Function-like Element of K6(K7(NAT, the carrier of (TopSpaceMetr P)))
P1 . (lim S1) is set
S00 is Relation-like NAT -defined the carrier of P -valued Function-like V33( NAT , the carrier of P) Element of K6(K7(NAT, the carrier of P))
t1 is Element of the carrier of P
n4 is V11() real ext-real Element of REAL
rs0 is V11() real ext-real Element of REAL
r0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
S00 . m is Element of the carrier of P
dist ((S00 . m),t1) is V11() real ext-real Element of REAL
dom S00 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
S1 . m is Element of the carrier of (Closed-Interval-MSpace (0,1))
P1 . (S1 . m) is set
dist ((lim S1),(S1 . m)) is V11() real ext-real Element of REAL
n4 is V11() real ext-real set
(upper_bound r1) + n4 is V11() real ext-real Element of REAL
r2 - (upper_bound r1) is V11() real ext-real Element of REAL
r2 - (upper_bound r1) is V11() real ext-real Element of REAL
min ((r2 - (upper_bound r1)),n4) is V11() real ext-real set
(min ((r2 - (upper_bound r1)),n4)) / 2 is V11() real ext-real Element of REAL
(upper_bound r1) + ((min ((r2 - (upper_bound r1)),n4)) / 2) is V11() real ext-real Element of REAL
(upper_bound r1) + (min ((r2 - (upper_bound r1)),n4)) is V11() real ext-real Element of REAL
(upper_bound r1) + (r2 - (upper_bound r1)) is V11() real ext-real Element of REAL
P1 . ((upper_bound r1) + ((min ((r2 - (upper_bound r1)),n4)) / 2)) is set
r2 - (upper_bound r1) is V11() real ext-real Element of REAL
r2 - (upper_bound r1) is V11() real ext-real Element of REAL
rs0 is V11() real ext-real set
lim S00 is Element of the carrier of P
n4 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
S00 . n4 is Element of the carrier of P
dom s2 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
s2 . n4 is V11() real ext-real Element of REAL
dom S00 is V168() V169() V170() V171() V172() V173() Element of K6(NAT)
rs0 is V11() real ext-real Element of REAL
P1 . rs0 is set
P is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V120() V121() V168() V169() V170() V171() V172() V173() Element of NAT
TOP-REAL P is non empty TopSpace-like V134() V180() V181() V182() V183() V184() V185() V186() V192() L15()
the carrier of (TOP-REAL P) is non empty set
K6( the carrier of (TOP-REAL P)) is set
P1 is V43(P) V117() V160() Element of the carrier of (TOP-REAL P)
U2 is V43(P) V117() V160() Element of the carrier of (TOP-REAL P)
U3 is non empty Element of K6( the carrier of (TOP-REAL P))
f is non empty Element of K6( the carrier of (TOP-REAL P))
P is non empty compact Element of K6( the carrier of (TOP-REAL 2))
W-min P is V43(2) V117() V160() Element of the carrier of (TOP-REAL 2)
E-max P is V43(2) V117() V160() Element of the carrier of (TOP-REAL 2)
P1 is non empty compact Element of K6( the carrier of (TOP-REAL 2))
Upper_Arc P is non empty Element of K6( the carrier of (TOP-REAL 2))
Lower_Arc P is non empty Element of K6( the carrier of (TOP-REAL 2))
(TOP-REAL 2) | P is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P) is non empty set
[#] ((TOP-REAL 2) | P) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P))
K6( the carrier of ((TOP-REAL 2) | P)) is set
U2 is Element of K6( the carrier of ((TOP-REAL 2) | P))
(Upper_Arc P) /\ P is Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc P) \/ (Lower_Arc P) is non empty Element of K6( the carrier of (TOP-REAL 2))
U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))
(Lower_Arc P) /\ P is Element of K6( the carrier of (TOP-REAL 2))
(Upper_Arc P) /\ (Lower_Arc P) is Element of K6( the carrier of (TOP-REAL 2))
{(W-min P),(E-max P)} is non empty set
(TOP-REAL 2) | P1 is non empty strict TopSpace-like SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | P1) is non empty set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1))) is set
f is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P1) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P1)))
f . 0 is set
f . 1 is set
dom f is V168() V169() V170() Element of K6( the carrier of I[01])
K6( the carrier of I[01]) is set
[#] I[01] is non proper closed V168() V169() V170() Element of K6( the carrier of I[01])
rng f is Element of K6( the carrier of ((TOP-REAL 2) | P1))
K6( the carrier of ((TOP-REAL 2) | P1)) is set
[#] ((TOP-REAL 2) | P1) is non empty non proper closed Element of K6( the carrier of ((TOP-REAL 2) | P1))
r2 is set
r1 is set
f . r1 is set
Q is V11() real ext-real Element of REAL
r2 is set
r1 is set
f . r1 is set
Q is V11() real ext-real Element of REAL
r2 is V11() real ext-real Element of REAL
f . r2 is set
r2 is V11() real ext-real Element of REAL
f . r2 is set
r1 is V11() real ext-real Element of REAL
f . r1 is set
r1 is V11() real ext-real Element of REAL
f . r1 is set
Euclid 2 is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of (Euclid 2) is non empty set
K6( the carrier of (Euclid 2)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
P1 \/ P is non empty Element of K6( the carrier of (TOP-REAL 2))
U2 \/ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))
Q is non empty Element of K6( the carrier of (Euclid 2))
(Euclid 2) | Q is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of Euclid 2
the carrier of ((Euclid 2) | Q) is non empty set
TopSpaceMetr ((Euclid 2) | Q) is non empty strict TopSpace-like TopStruct
g is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
U2 /\ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))
r0 is V11() real ext-real Element of REAL
g . r0 is set
Euclid 2 is non empty strict Reflexive discerning V86() triangle Discerning MetrStruct
the carrier of (Euclid 2) is non empty set
K6( the carrier of (Euclid 2)) is set
K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) is set
K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P))) is set
P1 \/ P is non empty Element of K6( the carrier of (TOP-REAL 2))
U2 \/ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))
Q is non empty Element of K6( the carrier of (Euclid 2))
(Euclid 2) | Q is non empty strict Reflexive discerning V86() triangle Discerning SubSpace of Euclid 2
the carrier of ((Euclid 2) | Q) is non empty set
TopSpaceMetr ((Euclid 2) | Q) is non empty strict TopSpace-like TopStruct
g is Relation-like the carrier of I[01] -defined the carrier of ((TOP-REAL 2) | P) -valued Function-like V33( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)) Element of K6(K7( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
U2 /\ U3 is Element of K6( the carrier of ((TOP-REAL 2) | P))
r0 is V11() real ext-real Element of REAL
g . r0 is set
r2 is V11() real ext-real Element of REAL
f . r2 is set
r2 is V11() real ext-real Element of REAL
f . r2 is set
r2 is V11() real ext-real Element of REAL
f . r2 is set
r2 is V11() real ext-real Element of REAL
f . r2 is set