:: 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

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

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

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

c

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

S2 . c

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

S9 . c

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

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

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

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

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

c

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

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

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

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

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

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

min c

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

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

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

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

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

c

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