:: FRECHET2 semantic presentation

REAL is non empty non trivial non finite V124() V125() V126() V130() V137() V138() V140() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V50() V51() V124() V125() V126() V127() V128() V129() V130() V135() V137() Element of K10(REAL)
K10(REAL) is non empty non trivial non finite set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V50() V51() V124() V125() V126() V127() V128() V129() V130() V135() V137() set
K10(NAT) is non empty non trivial non finite set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V135() V136() V137() V138() V139() Element of NAT
INT is non empty non trivial non finite V124() V125() V126() V127() V128() V130() set
K11(1,1) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
RAT is non empty non trivial non finite V124() V125() V126() V127() V130() set
K10(K11(1,1)) is non empty finite V49() set
K11(K11(1,1),1) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
K10(K11(K11(1,1),1)) is non empty finite V49() set
K11(K11(1,1),REAL) is non empty non trivial complex-valued ext-real-valued real-valued non finite set
K10(K11(K11(1,1),REAL)) is non empty non trivial non finite set
K11(REAL,REAL) is non empty non trivial complex-valued ext-real-valued real-valued non finite set
K11(K11(REAL,REAL),REAL) is non empty non trivial complex-valued ext-real-valued real-valued non finite set
K10(K11(K11(REAL,REAL),REAL)) is non empty non trivial non finite set
2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V135() V136() V137() V138() V139() Element of NAT
K11(2,2) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued finite set
K11(K11(2,2),REAL) is non empty non trivial complex-valued ext-real-valued real-valued non finite set
K10(K11(K11(2,2),REAL)) is non empty non trivial non finite set
K11(NAT,REAL) is non empty non trivial complex-valued ext-real-valued real-valued non finite set
K10(K11(NAT,REAL)) is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V124() V130() set
K10(NAT) is non empty non trivial non finite set
K11(COMPLEX,COMPLEX) is non empty non trivial complex-valued non finite set
K10(K11(COMPLEX,COMPLEX)) is non empty non trivial non finite set
K11(COMPLEX,REAL) is non empty non trivial complex-valued ext-real-valued real-valued non finite set
K10(K11(COMPLEX,REAL)) is non empty non trivial non finite set
{} is set
the empty Function-like functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V34() finite V49() V50() V52( {} ) real V124() V125() V126() V127() V128() V129() V130() V137() V138() V139() V140() set is empty Function-like functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V34() finite V49() V50() V52( {} ) real V124() V125() V126() V127() V128() V129() V130() V137() V138() V139() V140() set
K11(NAT,NAT) is non empty non trivial INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued non finite set
K10(K11(NAT,NAT)) is non empty non trivial non finite set
0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is Element of the carrier of T
{S} is non empty trivial finite V52(1) Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Cl {S} is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is Element of the carrier of T
{S} is non empty trivial finite V52(1) Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Cl {S} is Element of K10( the carrier of T)
x is set
Y is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is Element of the carrier of T
x is Element of the carrier of T
{S} is non empty trivial finite V52(1) Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Cl {S} is Element of K10( the carrier of T)
NAT --> S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
n0 is Element of K10( the carrier of T)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
(NAT --> S) . S9 is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is Element of the carrier of T
{S} is non empty trivial finite V52(1) Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
T is non empty 1-sorted
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
x is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
S * x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
id NAT is non empty Relation-like NAT -defined NAT -valued INT -valued RAT -valued Function-like one-to-one V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
T is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
T is non empty 1-sorted
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
K10( the carrier of T) is non empty set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of K10( the carrier of T)
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
rng Y is Element of K10( the carrier of T)
n0 is set
dom Y is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S9 is set
Y . S9 is set
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . S2 is Element of the carrier of T
T is non empty 1-sorted
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
K10( the carrier of T) is non empty set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S is Element of K10( the carrier of T)
x is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
x \/ Y is Element of K10( the carrier of T)
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
max (n0,S9) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . S2 is Element of the carrier of T
dom S is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
S is Element of the carrier of T
x is non empty open V111(T,S) Element of K10(K10( the carrier of T))
K11(NAT,x) is non empty non trivial non finite set
K10(K11(NAT,x)) is non empty non trivial non finite set
Y is non empty Relation-like NAT -defined x -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT,x))
rng Y is Element of K10(x)
K10(x) is non empty set
n0 is set
succ n0 is non empty set
Y .: (succ n0) is Element of K10(x)
meet (Y .: (succ n0)) is set
n0 is Relation-like Function-like set
dom n0 is set
rng n0 is set
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
S9 is set
S2 is set
n0 . S2 is set
succ S2 is non empty set
Y .: (succ S2) is Element of K10(x)
S29 is Element of K10(K10( the carrier of T))
meet S29 is Element of K10( the carrier of T)
meet (Y .: (succ S2)) is set
S9 is Element of K10(K10( the carrier of T))
S2 is Element of K10(K10( the carrier of T))
succ 0 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
Y .: (succ 0) is finite Element of K10(x)
meet (Y .: (succ 0)) is set
S29 is set
n0 . 0 is set
Intersect S2 is Element of K10( the carrier of T)
meet S2 is Element of K10( the carrier of T)
S29 is set
S29 is set
P is set
n0 . P is set
dom Y is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
succ P is non empty set
Y . P is set
Y .: (succ P) is Element of K10(x)
S1 is set
S1 is set
Y . S1 is set
c₁₂ is Element of K10( the carrier of T)
l is Element of K10( the carrier of T)
meet (Y .: (succ P)) is set
S29 is set
the topology of T is Element of K10(K10( the carrier of T))
S29 is set
P is set
n0 . P is set
succ P is non empty set
Y .: (succ P) is Element of K10(x)
S1 is Element of K10(K10( the carrier of T))
c₁₂ is Element of K10( the carrier of T)
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
succ S1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
meet S1 is Element of K10( the carrier of T)
meet (Y .: (succ P)) is set
S29 is Element of K10( the carrier of T)
P is Element of K10( the carrier of T)
dom Y is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S1 is set
Y . S1 is set
n0 . S1 is set
S1 is Element of K10( the carrier of T)
c₁₂ is Element of K10( the carrier of T)
succ S1 is non empty set
Y .: (succ S1) is Element of K10(x)
meet (Y .: (succ S1)) is set
S29 is non empty open V111(T,S) Element of K10(K10( the carrier of T))
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 . S1 is set
n0 . P is set
P + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
succ P is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
succ S1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
Y .: (succ P) is finite Element of K10(x)
Y .: (succ S1) is finite Element of K10(x)
dom Y is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
Y . P is Element of x
meet (Y .: (succ S1)) is set
meet (Y .: (succ P)) is set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 . S1 is set
n0 . P is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
S is Element of the carrier of T
NAT --> S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of the carrier of T
Lim Y is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
x is Element of the carrier of T
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Y is Element of the carrier of T
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
x is Element of the carrier of T
Y is Element of the carrier of T
x is Element of the carrier of T
Y is Element of the carrier of T
n0 is Element of K10( the carrier of T)
S9 is Element of K10( the carrier of T)
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
max (S2,S29) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . P is Element of the carrier of T
n0 /\ S9 is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
x is Element of the carrier of T
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Y is Element of the carrier of T
K10( the carrier of T) is non empty set
S is Element of the carrier of T
x is Element of the carrier of T
K10(K10( the carrier of T)) is non empty set
Y is non empty open V111(T,S) Element of K10(K10( the carrier of T))
n0 is non empty open V111(T,x) Element of K10(K10( the carrier of T))
S9 is Relation-like Function-like set
dom S9 is set
rng S9 is set
S9 is Relation-like Function-like set
dom S9 is set
rng S9 is set
S2 is Relation-like Function-like set
dom S2 is set
rng S2 is set
S2 is Relation-like Function-like set
dom S2 is set
rng S2 is set
S29 is set
S9 . S29 is set
S2 . S29 is set
(S9 . S29) /\ (S2 . S29) is set
the Element of (S9 . S29) /\ (S2 . S29) is Element of (S9 . S29) /\ (S2 . S29)
S1 is Element of K10( the carrier of T)
S1 is Element of K10( the carrier of T)
l is Element of K10( the carrier of T)
c₁₂ is Element of K10( the carrier of T)
c₁₂ /\ l is Element of K10( the carrier of T)
S29 is Relation-like Function-like set
dom S29 is set
rng S29 is set
P is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
S1 is Element of K10( the carrier of T)
S1 is Element of K10( the carrier of T)
c₁₂ is set
S2 . c₁₂ is set
l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
B is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P . B is Element of the carrier of T
P . B is Element of the carrier of T
S9 . B is set
S2 . B is set
(S9 . B) /\ (S2 . B) is set
S2 . l is set
Lim P is Element of K10( the carrier of T)
S1 is Element of K10( the carrier of T)
S1 is Element of K10( the carrier of T)
c₁₂ is set
S9 . c₁₂ is set
l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
B is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P . B is Element of the carrier of T
P . B is Element of the carrier of T
S9 . B is set
S2 . B is set
(S9 . B) /\ (S2 . B) is set
S9 . l is set
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
the Element of Lim S is Element of Lim S
Y is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is Element of K10( the carrier of T)
x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng x is Element of K10( the carrier of T)
Lim x is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of the carrier of T
K10( the carrier of T) is non empty set
Y is Element of K10( the carrier of T)
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of n0
S2 is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
n0 * S2 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of n0
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . S29 is Element of the carrier of T
dom S9 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S2 . S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 . (S2 . S29) is Element of the carrier of T
S2 is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K11( the carrier of T, the carrier of S) is non empty set
K10(K11( the carrier of T, the carrier of S)) is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
K11(NAT, the carrier of S) is non empty non trivial non finite set
K10(K11(NAT, the carrier of S)) is non empty non trivial non finite set
x is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V17( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of S))
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x * Y is non empty Relation-like NAT -defined the carrier of S -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of S))
Lim Y is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
x .: (Lim Y) is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
n0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of S))
Lim n0 is Element of K10( the carrier of S)
S9 is set
S2 is Element of the carrier of S
S29 is Element of K10( the carrier of S)
dom x is Element of K10( the carrier of T)
P is set
x . P is set
x " S29 is Element of K10( the carrier of T)
[#] S is non empty non proper Element of K10( the carrier of S)
S1 is Element of K10( the carrier of T)
S1 is Element of the carrier of T
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 . l is Element of the carrier of S
Y . l is Element of the carrier of T
x . (Y . l) is Element of the carrier of S
dom Y is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
n0 . l is Element of the carrier of S
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K11( the carrier of T, the carrier of S) is non empty set
K10(K11( the carrier of T, the carrier of S)) is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
K11(NAT, the carrier of S) is non empty non trivial non finite set
K10(K11(NAT, the carrier of S)) is non empty non trivial non finite set
x is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V17( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of S))
n0 is non empty Relation-like NAT -defined the carrier of S -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of S))
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x * Y is non empty Relation-like NAT -defined the carrier of S -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of S))
Lim Y is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
x .: (Lim Y) is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
Lim n0 is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
Y is Element of K10( the carrier of S)
x " Y is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
n0 is Element of K10( the carrier of T)
S2 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S2 is Element of K10( the carrier of T)
Lim S2 is Element of K10( the carrier of T)
x * S2 is non empty Relation-like NAT -defined the carrier of S -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of S))
rng (x * S2) is Element of K10( the carrier of S)
S9 is Element of K10( the carrier of S)
P is set
dom (x * S2) is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S1 is set
(x * S2) . S1 is set
dom S2 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S2 . S1 is set
x . (S2 . S1) is set
Lim (x * S2) is Element of K10( the carrier of S)
P is set
dom x is Element of K10( the carrier of T)
x .: (Lim S2) is Element of K10( the carrier of S)
x . P is set
T is non empty TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is Element of K10( the carrier of T)
{ b₁ where b₁ is Element of the carrier of T : S₁[b₁] } is set
x is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
n0 is Element of the carrier of T
S9 is Element of the carrier of T
S2 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S2 is Element of K10( the carrier of T)
Lim S2 is Element of K10( the carrier of T)
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S9 is Element of K10( the carrier of T)
Lim S9 is Element of K10( the carrier of T)
x is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
n0 is Element of the carrier of T
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S9 is Element of K10( the carrier of T)
Lim S9 is Element of K10( the carrier of T)
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S9 is Element of K10( the carrier of T)
Lim S9 is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is Element of K10( the carrier of T)
Cl S is Element of K10( the carrier of T)
x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng x is Element of K10( the carrier of T)
Lim x is Element of K10( the carrier of T)
Y is Element of the carrier of T
n0 is Element of K10( the carrier of T)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
dom x is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
x . S9 is Element of the carrier of T
S /\ n0 is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
S is Element of K10( the carrier of T)
(T,S) is Element of K10( the carrier of T)
Cl S is Element of K10( the carrier of T)
x is set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
Y is Element of the carrier of T
n0 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng n0 is Element of K10( the carrier of T)
Lim n0 is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
Y is Element of the carrier of T
K10( the carrier of T) is non empty set
n0 is Element of K10( the carrier of T)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
x . S2 is Element of the carrier of T
dom x is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S29 is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
S * S29 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
S29 . S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . (S29 . S2) is Element of the carrier of T
x . S2 is Element of the carrier of T
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
Lim x is Element of K10( the carrier of T)
Y is set
n0 is Element of the carrier of T
T is non empty TopStruct
{} T is empty proper Function-like functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V34() finite V49() V50() V52( {} ) real V124() V125() V126() V127() V128() V129() V130() V137() V138() V139() V140() Element of K10( the carrier of T)
the carrier of T is non empty set
K10( the carrier of T) is non empty set
(T,({} T)) is Element of K10( the carrier of T)
the Element of (T,({} T)) is Element of (T,({} T))
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
x is Element of the carrier of T
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng Y is Element of K10( the carrier of T)
Lim Y is Element of K10( the carrier of T)
dom Y is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
T is non empty TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
S is Element of K10( the carrier of T)
(T,S) is Element of K10( the carrier of T)
x is set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
Y is Element of the carrier of T
NAT --> Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng (NAT --> Y) is Element of K10( the carrier of T)
Lim (NAT --> Y) is Element of K10( the carrier of T)
{Y} is non empty trivial finite V52(1) Element of K10( the carrier of T)
S9 is set
n0 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng n0 is Element of K10( the carrier of T)
Lim n0 is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
S is Element of K10( the carrier of T)
(T,S) is Element of K10( the carrier of T)
x is Element of K10( the carrier of T)
(T,x) is Element of K10( the carrier of T)
(T,S) \/ (T,x) is Element of K10( the carrier of T)
S \/ x is Element of K10( the carrier of T)
(T,(S \/ x)) is Element of K10( the carrier of T)
Y is set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
n0 is Element of the carrier of T
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S9 is Element of K10( the carrier of T)
Lim S9 is Element of K10( the carrier of T)
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
n0 is Element of the carrier of T
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S9 is Element of K10( the carrier of T)
Lim S9 is Element of K10( the carrier of T)
Y is set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
n0 is Element of the carrier of T
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S9 is Element of K10( the carrier of T)
Lim S9 is Element of K10( the carrier of T)
S2 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S9
rng S2 is Element of K10( the carrier of T)
Lim S2 is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
S is Element of K10( the carrier of T)
Cl S is Element of K10( the carrier of T)
(T,S) is Element of K10( the carrier of T)
Y is set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
x is Element of K10( the carrier of T)
n0 is Element of the carrier of T
S9 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S9 is Element of K10( the carrier of T)
Lim S9 is Element of K10( the carrier of T)
S is Element of K10( the carrier of T)
Cl S is Element of K10( the carrier of T)
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
x is Element of the carrier of T
(T,S) is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
{} T is empty proper Function-like functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V34() finite V49() V50() V52( {} ) real V124() V125() V126() V127() V128() V129() V130() V137() V138() V139() V140() Element of K10( the carrier of T)
(T,({} T)) is Element of K10( the carrier of T)
S is Element of K10( the carrier of T)
(T,S) is Element of K10( the carrier of T)
x is Element of K10( the carrier of T)
S \/ x is Element of K10( the carrier of T)
(T,(S \/ x)) is Element of K10( the carrier of T)
(T,x) is Element of K10( the carrier of T)
(T,S) \/ (T,x) is Element of K10( the carrier of T)
(T,(T,S)) is Element of K10( the carrier of T)
Cl S is Element of K10( the carrier of T)
(T,(Cl S)) is Element of K10( the carrier of T)
Cl (Cl S) is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is Element of K10( the carrier of T)
Cl S is Element of K10( the carrier of T)
(T,S) is Element of K10( the carrier of T)
x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng x is Element of K10( the carrier of T)
Lim x is Element of K10( the carrier of T)
Y is set
n0 is Element of the carrier of T
(T,(T,S)) is Element of K10( the carrier of T)
x is Element of the carrier of T
x is Element of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
{} T is empty proper Function-like functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V34() finite V49() V50() V52( {} ) real V124() V125() V126() V127() V128() V129() V130() V137() V138() V139() V140() Element of K10( the carrier of T)
(T,({} T)) is Element of K10( the carrier of T)
S is Element of K10( the carrier of T)
(T,S) is Element of K10( the carrier of T)
x is Element of K10( the carrier of T)
Y is Element of K10( the carrier of T)
x \/ Y is Element of K10( the carrier of T)
(T,(x \/ Y)) is Element of K10( the carrier of T)
(T,x) is Element of K10( the carrier of T)
(T,Y) is Element of K10( the carrier of T)
(T,x) \/ (T,Y) is Element of K10( the carrier of T)
n0 is Element of K10( the carrier of T)
(T,n0) is Element of K10( the carrier of T)
(T,(T,n0)) is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
x is Element of the carrier of T
{x} is non empty trivial finite V52(1) Element of K10( the carrier of T)
x is Element of the carrier of T
{x} is non empty trivial finite V52(1) Element of K10( the carrier of T)
x is Element of the carrier of T
Y is Element of the carrier of T
n0 is Element of the carrier of T
{n0} is non empty trivial finite V52(1) Element of K10( the carrier of T)
n0 is Element of the carrier of T
{n0} is non empty trivial finite V52(1) Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
x is Element of the carrier of T
{x} is non empty trivial finite V52(1) Element of K10( the carrier of T)
Y is set
n0 is Element of the carrier of T
Y is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
(T,S) is Element of the carrier of T
x is Element of the carrier of T
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Y is Element of the carrier of T
{Y} is non empty trivial finite V52(1) Element of K10( the carrier of T)
Lim S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Y is Element of the carrier of T
{Y} is non empty trivial finite V52(1) Element of K10( the carrier of T)
T is MetrStruct
the carrier of T is set
K11(NAT, the carrier of T) is set
K10(K11(NAT, the carrier of T)) is non empty set
TopSpaceMetr T is strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr T) is set
K11(NAT, the carrier of (TopSpaceMetr T)) is set
K10(K11(NAT, the carrier of (TopSpaceMetr T))) is non empty set
S is Relation-like NAT -defined the carrier of T -valued Function-like quasi_total Element of K10(K11(NAT, the carrier of T))
T is non empty MetrStruct
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr T) is non empty set
K11(NAT, the carrier of (TopSpaceMetr T)) is non empty non trivial non finite set
K10(K11(NAT, the carrier of (TopSpaceMetr T))) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr T) -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of (TopSpaceMetr T)))
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
T is non empty Reflexive discerning V99() triangle Discerning MetrStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr T) is non empty set
K11(NAT, the carrier of (TopSpaceMetr T)) is non empty non trivial non finite set
K10(K11(NAT, the carrier of (TopSpaceMetr T))) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of the carrier of T
Y is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr T) -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of (TopSpaceMetr T)))
n0 is Element of the carrier of (TopSpaceMetr T)
K10( the carrier of (TopSpaceMetr T)) is non empty set
S9 is Element of K10( the carrier of (TopSpaceMetr T))
S2 is ext-real V34() real set
Ball (x,S2) is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
S29 is ext-real V34() real Element of REAL
Ball (x,S29) is Element of K10( the carrier of T)
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . S1 is Element of the carrier of (TopSpaceMetr T)
S . S1 is Element of the carrier of T
Y . S1 is Element of the carrier of (TopSpaceMetr T)
K10( the carrier of T) is non empty set
Family_open_set T is Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
S9 is Element of K10( the carrier of T)
K10( the carrier of (TopSpaceMetr T)) is non empty set
S2 is Element of K10( the carrier of (TopSpaceMetr T))
S29 is Element of K10( the carrier of (TopSpaceMetr T))
the topology of (TopSpaceMetr T) is Element of K10(K10( the carrier of (TopSpaceMetr T)))
K10(K10( the carrier of (TopSpaceMetr T))) is non empty set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . S1 is Element of the carrier of T
T is non empty Reflexive discerning V99() triangle Discerning MetrStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr T) is non empty set
K11(NAT, the carrier of (TopSpaceMetr T)) is non empty non trivial non finite set
K10(K11(NAT, the carrier of (TopSpaceMetr T))) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr T) -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of (TopSpaceMetr T)))
Y is Element of the carrier of T
n0 is Element of the carrier of (TopSpaceMetr T)
Y is Element of the carrier of (TopSpaceMetr T)
n0 is Element of the carrier of T
T is non empty Reflexive discerning V99() triangle Discerning MetrStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
TopSpaceMetr T is non empty strict TopSpace-like TopStruct
the carrier of (TopSpaceMetr T) is non empty set
K11(NAT, the carrier of (TopSpaceMetr T)) is non empty non trivial non finite set
K10(K11(NAT, the carrier of (TopSpaceMetr T))) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
lim S is Element of the carrier of T
x is non empty Relation-like NAT -defined the carrier of (TopSpaceMetr T) -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of (TopSpaceMetr T)))
((TopSpaceMetr T),x) is Element of the carrier of (TopSpaceMetr T)
n0 is Element of the carrier of (TopSpaceMetr T)
T is TopStruct
the carrier of T is set
K11(NAT, the carrier of T) is set
K10(K11(NAT, the carrier of T)) is non empty set
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of the carrier of T
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
K10( the carrier of T) is non empty set
n0 is Element of K10( the carrier of T)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
max (S2,S9) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . (max (S2,S9)) is Element of the carrier of T
P is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
S * P is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
P . (max (S2,S9)) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . (P . (max (S2,S9))) is Element of the carrier of T
dom P is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of the carrier of T
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
K10( the carrier of T) is non empty set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S is Element of K10( the carrier of T)
x is Element of the carrier of T
{ b₁ where b₁ is Element of the carrier of T : x in Cl {b₁} } is set
Y is Element of K10( the carrier of T)
n0 is Element of K10( the carrier of T)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . S9 is Element of the carrier of T
dom S is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S . S9 is Element of the carrier of T
S2 is Element of the carrier of T
{S2} is non empty trivial finite V52(1) Element of K10( the carrier of T)
Cl {S2} is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Y is Element of the carrier of T
x is Element of the carrier of T
{Y} is non empty trivial finite V52(1) Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Cl {Y} is Element of K10( the carrier of T)
n0 is Element of K10( the carrier of T)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . S9 is Element of the carrier of T
{Y} /\ n0 is finite Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is Element of the carrier of T
{ b₁ where b₁ is Element of the carrier of T : S in Cl {b₁} } is set
x is Element of K10( the carrier of T)
Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng Y is Element of K10( the carrier of T)
(rng Y) /\ x is Element of K10( the carrier of T)
n0 is set
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 is Element of the carrier of T
{S9} is non empty trivial finite V52(1) Element of K10( the carrier of T)
Cl {S9} is Element of K10( the carrier of T)
S2 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of Y
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 is set
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . P is Element of the carrier of T
Y . S2 is Element of the carrier of T
dom Y is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
Y . S9 is set
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . S1 is Element of the carrier of T
Y . S29 is Element of the carrier of T
n0 is Relation-like Function-like set
dom n0 is set
n0 . 0 is set
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 . S9 is set
S9 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 - 1 is ext-real V34() real set
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 . S9 is set
S9 is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . (S2 + 1) is ext-real V34() real Element of REAL
S9 . S2 is ext-real V34() real Element of REAL
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . P is Element of the carrier of T
S2 is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
Y * S2 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of Y
S29 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of Y
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 . P is Element of the carrier of T
S29 . S1 is Element of the carrier of T
S2 . P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
dom S29 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S2 . S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . (S2 . S1) is Element of the carrier of T
P + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 . (P + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y . S1 is Element of the carrier of T
P is set
dom S29 is set
S1 is set
S29 . P is set
S29 . S1 is set
dom S29 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng x is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S is Element of K10( the carrier of T)
Y is set
x . Y is set
dom x is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
dom S is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
n0 is set
S . n0 is set
Y is Relation-like Function-like set
dom Y is set
rng Y is set
S9 is set
S2 is set
Y . S9 is set
Y . S2 is set
x . S2 is set
S . (Y . S2) is set
x . S9 is set
dom x is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= S9 ) } is set
S9 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 is set
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : not S9 + 1 <= b₁ } is set
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= S9 ) } is set
S2 is set
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 is set
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= S29 ) } is set
S1 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S1 is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₂ is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= l ) } is set
S29 is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= P ) } is set
n0 is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 is Relation-like Function-like set
dom S9 is set
S9 . 0 is set
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . S2 is set
S2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . (S2 + 1) is set
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= S29 ) } is set
S1 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S1 is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . S2 is set
S29 is ext-real V34() real Element of REAL
S2 is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 . (S29 + 1) is ext-real V34() real Element of REAL
S2 . S29 is ext-real V34() real Element of REAL
S9 . S29 is set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= P ) } is set
S1 is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
rng S9 is set
S29 is set
P is set
S9 . P is set
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . S1 is set
S29 is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
P is set
dom S29 is set
S1 is set
S29 . P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
S29 . S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
dom S29 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S29 . P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real Element of REAL
S29 . S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real Element of REAL
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 " is Relation-like Function-like set
rng (S9 ") is set
P is set
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 . S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 . (S1 + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . S1 is set
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= c₁₂ ) } is set
S9 . (S1 + 1) is set
l is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 . 0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is set
c₁₂ is set
S9 . c₁₂ is set
l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 . l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : not S1 <= b₁ } is set
P is set
S1 is set
S9 . S1 is set
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
0 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 - 1 is ext-real V34() real set
c₁₂ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . c₁₂ is set
l is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : ( b₁ in rng Y & not b₁ <= l ) } is set
c₁₂ + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S9 . S1 is set
B is non empty V124() V125() V126() V127() V128() V129() V135() V137() Element of K10(NAT)
min B is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
c₁₅ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
dom (S9 ") is set
Y * (S9 ") is Relation-like Function-like set
dom (Y * (S9 ")) is set
rng (Y * (S9 ")) is set
P is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
rng P is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S1 is non empty Relation-like NAT -defined NAT -valued Function-like one-to-one V17( NAT ) quasi_total onto bijective complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
S1 " is non empty Relation-like NAT -defined NAT -valued Function-like one-to-one V17( NAT ) quasi_total onto bijective complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
x * (S1 ") is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
dom (x * (S1 ")) is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S9 * S is Relation-like Function-like set
dom (S9 * S) is set
dom S is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S1 is set
(x * (S1 ")) . S1 is set
(S9 * S) . S1 is set
S9 . S1 is set
Y " is Relation-like Function-like set
(Y ") . (S9 . S1) is set
dom (S1 ") is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
(Y * (S9 ")) " is Relation-like Function-like set
((Y * (S9 ")) ") . S1 is set
x . (((Y * (S9 ")) ") . S1) is set
(S9 ") " is Relation-like Function-like set
((S9 ") ") * (Y ") is Relation-like Function-like set
(((S9 ") ") * (Y ")) . S1 is set
x . ((((S9 ") ") * (Y ")) . S1) is set
S9 * (Y ") is Relation-like Function-like set
(S9 * (Y ")) . S1 is set
x . ((S9 * (Y ")) . S1) is set
x . ((Y ") . (S9 . S1)) is set
Y . ((Y ") . (S9 . S1)) is set
S . (Y . ((Y ") . (S9 . S1))) is set
S . (S9 . S1) is set
S * S29 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
F₁() is non empty 1-sorted
the carrier of F₁() is non empty set
K11(NAT, the carrier of F₁()) is non empty non trivial non finite set
K10(K11(NAT, the carrier of F₁())) is non empty non trivial non finite set
F₂() is non empty Relation-like NAT -defined the carrier of F₁() -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of F₁()))
F₃() is non empty Relation-like NAT -defined NAT -valued Function-like one-to-one V17( NAT ) quasi_total onto bijective complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
F₂() * F₃() is non empty Relation-like NAT -defined the carrier of F₁() -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of F₁()))
T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
succ T is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
F₃() " is non empty Relation-like NAT -defined NAT -valued Function-like one-to-one V17( NAT ) quasi_total onto bijective complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
dom (F₃() ") is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
(F₃() ") . T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
(F₃() ") .: (succ T) is finite V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of K10(NAT)
S is non empty finite V124() V125() V126() V127() V128() V129() V135() V136() V137() V138() V139() Element of K10(NAT)
sup S is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() set
(sup S) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
(F₂() * F₃()) . Y is Element of the carrier of F₁()
dom F₃() is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
F₃() . Y is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
{ b₁ where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT : not T <= b₁ } is set
F₃() " (succ T) is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
F₂() . (F₃() . Y) is Element of the carrier of F₁()
F₁() is non empty TopStruct
the carrier of F₁() is non empty set
K11(NAT, the carrier of F₁()) is non empty non trivial non finite set
K10(K11(NAT, the carrier of F₁())) is non empty non trivial non finite set
F₂() is non empty Relation-like NAT -defined the carrier of F₁() -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of F₁()))
F₃() is non empty Relation-like NAT -defined NAT -valued Function-like one-to-one V17( NAT ) quasi_total onto bijective complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
F₂() * F₃() is non empty Relation-like NAT -defined the carrier of F₁() -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of F₁()))
T is non empty 1-sorted
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S * F₃() is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is non empty Relation-like NAT -defined NAT -valued Function-like one-to-one V17( NAT ) quasi_total onto bijective complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
S * x is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
Y is Element of the carrier of T
K10( the carrier of T) is non empty set
n0 is Element of K10( the carrier of T)
S9 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . S2 is Element of the carrier of T
S29 is Element of the carrier of T
T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued Element of K10(K11(NAT,REAL))
x is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
x + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . (x + 1) is ext-real V34() real Element of REAL
S . x is ext-real V34() real Element of REAL
(x + 1) + T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
x + T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
x is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . x is ext-real V34() real Element of REAL
x + T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
x is non empty Relation-like NAT -defined NAT -valued Function-like V17( NAT ) quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K10(K11(NAT,NAT))
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
x . Y is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
Y + T is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of the carrier of T
Y is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real set
S ^\ Y is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
K10( the carrier of T) is non empty set
S9 is Element of K10( the carrier of T)
S2 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S2 + Y is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . S29 is Element of the carrier of T
S29 - Y is ext-real V34() real set
P is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
(S ^\ Y) . P is Element of the carrier of T
(S29 - Y) + Y is ext-real V34() real set
S . ((S29 - Y) + Y) is set
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
Cl (rng S) is Element of K10( the carrier of T)
x is Element of the carrier of T
Y is Element of K10( the carrier of T)
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . n0 is Element of the carrier of T
dom S is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
(rng S) /\ Y is Element of K10( the carrier of T)
T is non empty TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set
S is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
x is Element of the carrier of T
K10( the carrier of T) is non empty set
{ b₁ where b₁ is Element of the carrier of T : S₁[b₁] } is set
Y is Element of K10( the carrier of T)
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
rng n0 is Element of K10( the carrier of T)
S9 is set
dom n0 is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
S2 is set
n0 . S2 is set
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 . S29 is Element of the carrier of T
Y is Element of K10( the carrier of T)
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S ^\ n0 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
rng (S ^\ n0) is Element of K10( the carrier of T)
Cl (rng (S ^\ n0)) is Element of K10( the carrier of T)
S2 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
rng S2 is Element of K10( the carrier of T)
Lim S2 is Element of K10( the carrier of T)
S29 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
(S ^\ n0) . S29 is Element of the carrier of T
S29 + n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
S . (S29 + n0) is Element of the carrier of T
(rng (S ^\ n0)) /\ Y is Element of K10( the carrier of T)
the Element of (rng (S ^\ n0)) /\ Y is Element of (rng (S ^\ n0)) /\ Y
dom (S ^\ n0) is V124() V125() V126() V127() V128() V129() V137() Element of K10(NAT)
P is set
(S ^\ n0) . P is set
S1 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
(S ^\ n0) . S1 is Element of the carrier of T
S29 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S2
rng S29 is Element of K10( the carrier of T)
P is non empty Relation-like NAT -defined NAT -valued Function-like one-to-one V17( NAT ) quasi_total onto bijective complex-valued ext-real-valued real-valued natural-valued Element of K10(K11(NAT,NAT))
S29 * P is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total Element of K10(K11(NAT, the carrier of T))
S1 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S ^\ n0
S1 is non empty Relation-like NAT -defined the carrier of T -valued Function-like V17( NAT ) quasi_total subsequence of S
Y is Element of K10( the carrier of T)
n0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() finite V50() real V122() V123() V124() V125() V126() V127() V128() V129() V137() V138() V139() Element of NAT
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is Element of the carrier of T
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
T is non empty TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K11(NAT, the carrier of T) is non empty non trivial non finite set
K10(K11(NAT, the carrier of T)) is non empty non trivial non finite set