:: ORDINAL4 semantic presentation

omega is epsilon-transitive epsilon-connected ordinal non empty V33() cardinal limit_cardinal set

bool omega is V33() set

{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set

the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set

1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega

succ {} is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega

{{}} is non empty trivial 1 -element set

{} \/ {{}} is non empty set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

last D is set

dom D is epsilon-transitive epsilon-connected ordinal set

union (dom D) is epsilon-transitive epsilon-connected ordinal set

D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

last D is epsilon-transitive epsilon-connected ordinal set

union (dom D) is epsilon-transitive epsilon-connected ordinal set

D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set

lim D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

succ f is epsilon-transitive epsilon-connected ordinal non empty set

{f} is non empty trivial 1 -element set

f \/ {f} is non empty set

D . f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

D . c is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like set

dom D is epsilon-transitive epsilon-connected ordinal set

f is Relation-like T-Sequence-like Function-like set

dom f is epsilon-transitive epsilon-connected ordinal set

(dom D) +^ (dom f) is epsilon-transitive epsilon-connected ordinal set

g is Relation-like Function-like set

dom g is set

C is Relation-like T-Sequence-like Function-like set

dom C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

C . c is set

D . c is set

c is epsilon-transitive epsilon-connected ordinal set

(dom D) +^ c is epsilon-transitive epsilon-connected ordinal set

C . ((dom D) +^ c) is set

f . c is set

((dom D) +^ c) -^ (dom D) is epsilon-transitive epsilon-connected ordinal set

f . (((dom D) +^ c) -^ (dom D)) is set

g is Relation-like T-Sequence-like Function-like set

dom g is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like set

dom C is epsilon-transitive epsilon-connected ordinal set

c is set

b is epsilon-transitive epsilon-connected ordinal set

g . b is set

D . b is set

g . c is set

C . c is set

b is epsilon-transitive epsilon-connected ordinal set

b -^ (dom D) is epsilon-transitive epsilon-connected ordinal set

(dom D) +^ (b -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set

g . b is set

f . (b -^ (dom D)) is set

g . c is set

C . c is set

g . c is set

C . c is set

g . c is set

C . c is set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

rng D is set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

(D,f) is Relation-like T-Sequence-like Function-like set

rng (D,f) is set

rng f is set

(rng D) \/ (rng f) is set

dom (D,f) is epsilon-transitive epsilon-connected ordinal set

dom D is epsilon-transitive epsilon-connected ordinal set

dom f is epsilon-transitive epsilon-connected ordinal set

(dom D) +^ (dom f) is epsilon-transitive epsilon-connected ordinal set

b is set

e is set

(D,f) . e is set

e is epsilon-transitive epsilon-connected ordinal set

D . e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e -^ (dom D) is epsilon-transitive epsilon-connected ordinal set

(dom D) +^ (e -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set

f . (e -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

(D,f) is Relation-like T-Sequence-like Function-like set

rng D is set

C is epsilon-transitive epsilon-connected ordinal set

rng f is set

c is epsilon-transitive epsilon-connected ordinal set

C +^ c is epsilon-transitive epsilon-connected ordinal set

C \/ c is epsilon-transitive epsilon-connected ordinal set

rng (D,f) is set

(rng D) \/ (rng f) is set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

(f,D) is Relation-like T-Sequence-like Function-like Ordinal-yielding set

g is epsilon-transitive epsilon-connected ordinal set

dom D is epsilon-transitive epsilon-connected ordinal set

dom (f,D) is epsilon-transitive epsilon-connected ordinal set

dom f is epsilon-transitive epsilon-connected ordinal set

(dom f) +^ (dom D) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

(dom f) +^ C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(f,D) . b is epsilon-transitive epsilon-connected ordinal set

b -^ c is epsilon-transitive epsilon-connected ordinal set

c +^ (b -^ c) is epsilon-transitive epsilon-connected ordinal set

C +^ (b -^ c) is epsilon-transitive epsilon-connected ordinal set

(dom f) +^ (C +^ (b -^ c)) is epsilon-transitive epsilon-connected ordinal set

D . (C +^ (b -^ c)) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(dom f) +^ b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

(f,D) . e is epsilon-transitive epsilon-connected ordinal set

e -^ e is epsilon-transitive epsilon-connected ordinal set

b +^ (e -^ e) is epsilon-transitive epsilon-connected ordinal set

e +^ (e -^ e) is epsilon-transitive epsilon-connected ordinal set

(dom f) +^ (b +^ (e -^ e)) is epsilon-transitive epsilon-connected ordinal set

D . (b +^ (e -^ e)) is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

g +^ f is epsilon-transitive epsilon-connected ordinal set

g +^ D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

dom (g +^ D) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

(g +^ D) . c is epsilon-transitive epsilon-connected ordinal set

D . c is epsilon-transitive epsilon-connected ordinal set

g +^ (D . c) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

(g +^ D) . e is epsilon-transitive epsilon-connected ordinal set

D . e is epsilon-transitive epsilon-connected ordinal set

g +^ (D . e) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

C -^ g is epsilon-transitive epsilon-connected ordinal set

c -^ g is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

g +^ (C -^ g) is epsilon-transitive epsilon-connected ordinal set

g +^ (c -^ g) is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

(g +^ D) . e is epsilon-transitive epsilon-connected ordinal set

D . e is epsilon-transitive epsilon-connected ordinal set

g +^ (D . e) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

g +^ b is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

succ f is epsilon-transitive epsilon-connected ordinal non empty set

{f} is non empty trivial 1 -element set

f \/ {f} is non empty set

g is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

f *^ g is epsilon-transitive epsilon-connected ordinal set

D *^ g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

dom (D *^ g) is epsilon-transitive epsilon-connected ordinal set

the epsilon-transitive epsilon-connected ordinal Element of dom D is epsilon-transitive epsilon-connected ordinal Element of dom D

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

(D *^ g) . e is epsilon-transitive epsilon-connected ordinal set

D . e is epsilon-transitive epsilon-connected ordinal set

(D . e) *^ g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(D *^ g) . b is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

(D . b) *^ g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b *^ g is epsilon-transitive epsilon-connected ordinal set

succ f is epsilon-transitive epsilon-connected ordinal non empty set

{f} is non empty trivial 1 -element set

f \/ {f} is non empty set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e *^ g is epsilon-transitive epsilon-connected ordinal set

(D *^ g) . b is epsilon-transitive epsilon-connected ordinal set

(D . b) *^ g is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

succ b is epsilon-transitive epsilon-connected ordinal non empty set

{b} is non empty trivial 1 -element set

b \/ {b} is non empty set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

(D *^ g) . b is epsilon-transitive epsilon-connected ordinal set

e *^ g is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

succ e is epsilon-transitive epsilon-connected ordinal non empty set

{e} is non empty trivial 1 -element set

e \/ {e} is non empty set

e is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

D . c is epsilon-transitive epsilon-connected ordinal set

f . c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

c is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

b \/ c is epsilon-transitive epsilon-connected ordinal set

D . (b \/ c) is epsilon-transitive epsilon-connected ordinal set

f . (b \/ c) is epsilon-transitive epsilon-connected ordinal set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

c is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

succ C is epsilon-transitive epsilon-connected ordinal non empty set

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

c \/ b is epsilon-transitive epsilon-connected ordinal set

f . (c \/ b) is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

D . (c \/ b) is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom g is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

C . b is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e \/ e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

D . e is epsilon-transitive epsilon-connected ordinal set

C . e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

g . e is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

sup D is epsilon-transitive epsilon-connected ordinal set

rng D is set

sup (rng D) is epsilon-transitive epsilon-connected ordinal set

lim D is epsilon-transitive epsilon-connected ordinal set

D . {} is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is set

D . b is set

e is epsilon-transitive epsilon-connected ordinal set

succ e is epsilon-transitive epsilon-connected ordinal non empty set

{e} is non empty trivial 1 -element set

e \/ {e} is non empty set

e is epsilon-transitive epsilon-connected ordinal non empty set

b is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

D . f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

D . f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D . C is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is epsilon-transitive epsilon-connected ordinal set

D " f is set

dom D is epsilon-transitive epsilon-connected ordinal set

g is set

D . g is set

c is set

C is epsilon-transitive epsilon-connected ordinal set

D . C is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

D . c is set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

D * f is Relation-like Function-like set

dom (D * f) is set

dom f is epsilon-transitive epsilon-connected ordinal set

D " (dom f) is set

rng f is set

C is epsilon-transitive epsilon-connected ordinal set

g is Relation-like T-Sequence-like Function-like set

rng g is set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f * D is Relation-like Function-like set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

C is epsilon-transitive epsilon-connected ordinal set

dom g is epsilon-transitive epsilon-connected ordinal set

g . C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

g . c is epsilon-transitive epsilon-connected ordinal set

f . C is epsilon-transitive epsilon-connected ordinal set

f . c is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

dom D is epsilon-transitive epsilon-connected ordinal set

dom f is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

D . e is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is epsilon-transitive epsilon-connected ordinal set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

rng g is set

sup (rng g) is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom C is epsilon-transitive epsilon-connected ordinal set

g * C is Relation-like Function-like set

dom D is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

dom g is epsilon-transitive epsilon-connected ordinal set

e is set

g . e is set

e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

D . b is epsilon-transitive epsilon-connected ordinal set

g . b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

C . e is epsilon-transitive epsilon-connected ordinal set

dom D is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

dom g is epsilon-transitive epsilon-connected ordinal set

b is set

g . b is set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

D . e is epsilon-transitive epsilon-connected ordinal set

g . e is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

C . c is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is epsilon-transitive epsilon-connected ordinal set

D | f is Relation-like rng D -valued T-Sequence-like Function-like Ordinal-yielding set

rng D is set

dom D is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

dom (D | f) is epsilon-transitive epsilon-connected ordinal set

(D | f) . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

(D | f) . C is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

D . C is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

sup D is epsilon-transitive epsilon-connected ordinal set

rng D is set

sup (rng D) is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is set

D . C is set

c is epsilon-transitive epsilon-connected ordinal set

succ c is epsilon-transitive epsilon-connected ordinal non empty set

{c} is non empty trivial 1 -element set

c \/ {c} is non empty set

D . (succ c) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

succ f is epsilon-transitive epsilon-connected ordinal non empty set

{f} is non empty trivial 1 -element set

f \/ {f} is non empty set

D is Relation-like Function-like set

rng D is set

f is Relation-like Function-like set

D * f is Relation-like Function-like set

g is set

f | g is Relation-like Function-like set

D * (f | g) is Relation-like Function-like set

D " (rng D) is set

dom D is set

D " g is set

dom (D * (f | g)) is set

dom (f | g) is set

D " (dom (f | g)) is set

dom f is set

(dom f) /\ g is set

D " ((dom f) /\ g) is set

D " (dom f) is set

(D " (dom f)) /\ (D " g) is set

dom (D * f) is set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

D * f is Relation-like Function-like set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

dom f is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

dom g is epsilon-transitive epsilon-connected ordinal set

g . C is epsilon-transitive epsilon-connected ordinal set

g | C is Relation-like rng g -valued T-Sequence-like Function-like Ordinal-yielding set

rng g is set

c is epsilon-transitive epsilon-connected ordinal set

D . C is epsilon-transitive epsilon-connected ordinal set

D | C is Relation-like rng D -valued T-Sequence-like Function-like Ordinal-yielding set

rng D is set

dom (D | C) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

lim (D | C) is epsilon-transitive epsilon-connected ordinal set

sup (D | C) is epsilon-transitive epsilon-connected ordinal set

rng (D | C) is set

sup (rng (D | C)) is epsilon-transitive epsilon-connected ordinal set

f . b is epsilon-transitive epsilon-connected ordinal set

f | b is Relation-like rng f -valued T-Sequence-like Function-like Ordinal-yielding set

rng f is set

dom (f | b) is epsilon-transitive epsilon-connected ordinal set

e is set

e is set

(D | C) . e is set

(D | C) * f is Relation-like Function-like set

(D | C) * (f | b) is Relation-like Function-like set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D . C is epsilon-transitive epsilon-connected ordinal set

f +^ C is epsilon-transitive epsilon-connected ordinal set

f +^ g is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D . C is epsilon-transitive epsilon-connected ordinal set

C *^ f is epsilon-transitive epsilon-connected ordinal set

g *^ f is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

exp ({},D) is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp ({},f) is epsilon-transitive epsilon-connected ordinal set

succ f is epsilon-transitive epsilon-connected ordinal non empty set

{f} is non empty trivial 1 -element set

f \/ {f} is non empty set

exp ({},(succ f)) is epsilon-transitive epsilon-connected ordinal set

{} *^ (exp ({},f)) is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp ({},f) is epsilon-transitive epsilon-connected ordinal set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega

c is epsilon-transitive epsilon-connected ordinal set

g . c is epsilon-transitive epsilon-connected ordinal set

exp ({},c) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

lim g is epsilon-transitive epsilon-connected ordinal set

exp ({},{}) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega

C is epsilon-transitive epsilon-connected ordinal set

f . C is epsilon-transitive epsilon-connected ordinal set

exp ({},C) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set

b is epsilon-transitive epsilon-connected ordinal set

f . b is epsilon-transitive epsilon-connected ordinal set

exp (1,b) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

exp (D,c) is epsilon-transitive epsilon-connected ordinal set

succ c is epsilon-transitive epsilon-connected ordinal non empty set

{c} is non empty trivial 1 -element set

c \/ {c} is non empty set

exp (D,(succ c)) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

1 *^ (exp (D,c)) is epsilon-transitive epsilon-connected ordinal set

D *^ (exp (D,c)) is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

exp (D,c) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

e is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom e is epsilon-transitive epsilon-connected ordinal set

e . b is epsilon-transitive epsilon-connected ordinal set

rng e is set

e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e . e is epsilon-transitive epsilon-connected ordinal set

e . b is epsilon-transitive epsilon-connected ordinal set

exp (D,e) is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

lim e is epsilon-transitive epsilon-connected ordinal set

sup e is epsilon-transitive epsilon-connected ordinal set

sup (rng e) is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

exp (D,c) is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

C . c is epsilon-transitive epsilon-connected ordinal set

C . b is epsilon-transitive epsilon-connected ordinal set

exp (D,c) is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

sup C is epsilon-transitive epsilon-connected ordinal set

rng C is set

sup (rng C) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (f,D) is epsilon-transitive epsilon-connected ordinal set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom g is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom C is epsilon-transitive epsilon-connected ordinal set

c is set

C . c is set

b is epsilon-transitive epsilon-connected ordinal set

exp (f,b) is epsilon-transitive epsilon-connected ordinal set

g . c is set

c is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

lim C is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

exp (D,(succ g)) is epsilon-transitive epsilon-connected ordinal set

D *^ (exp (D,g)) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom C is epsilon-transitive epsilon-connected ordinal set

lim C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

C . b is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

succ f is epsilon-transitive epsilon-connected ordinal non empty set

{f} is non empty trivial 1 -element set

f \/ {f} is non empty set

exp (D,(succ f)) is epsilon-transitive epsilon-connected ordinal set

1 *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

D *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

exp (D,C) is epsilon-transitive epsilon-connected ordinal set

c is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

c . b is epsilon-transitive epsilon-connected ordinal set

c . e is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

exp (D,e) is epsilon-transitive epsilon-connected ordinal set

sup c is epsilon-transitive epsilon-connected ordinal set

rng c is set

sup (rng c) is epsilon-transitive epsilon-connected ordinal set

lim c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

c . b is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

exp (D,C) is epsilon-transitive epsilon-connected ordinal set

succ C is epsilon-transitive epsilon-connected ordinal non empty set

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

exp (D,(succ C)) is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

exp (D,c) is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

exp (D,C) is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

D . C is epsilon-transitive epsilon-connected ordinal set

exp (f,C) is epsilon-transitive epsilon-connected ordinal set

exp (f,g) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom g is epsilon-transitive epsilon-connected ordinal set

sup g is epsilon-transitive epsilon-connected ordinal set

rng g is set

sup (rng g) is epsilon-transitive epsilon-connected ordinal set

lim g is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

exp (f,g) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

exp (D,C) is epsilon-transitive epsilon-connected ordinal set

exp (f,C) is epsilon-transitive epsilon-connected ordinal set

succ C is epsilon-transitive epsilon-connected ordinal non empty set

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

exp (D,(succ C)) is epsilon-transitive epsilon-connected ordinal set

exp (f,(succ C)) is epsilon-transitive epsilon-connected ordinal set

f *^ (exp (f,C)) is epsilon-transitive epsilon-connected ordinal set

D *^ (exp (D,C)) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

exp (D,C) is epsilon-transitive epsilon-connected ordinal set

exp (f,C) is epsilon-transitive epsilon-connected ordinal set

c is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom c is epsilon-transitive epsilon-connected ordinal set

b is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

c . e is epsilon-transitive epsilon-connected ordinal set

exp (D,e) is epsilon-transitive epsilon-connected ordinal set

b . e is epsilon-transitive epsilon-connected ordinal set

exp (f,e) is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

exp (f,{}) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

f +^ g is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ g)) is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

(exp (D,g)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

f +^ C is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ C)) is epsilon-transitive epsilon-connected ordinal set

exp (D,C) is epsilon-transitive epsilon-connected ordinal set

(exp (D,C)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

succ C is epsilon-transitive epsilon-connected ordinal non empty set

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

f +^ (succ C) is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ (succ C))) is epsilon-transitive epsilon-connected ordinal set

exp (D,(succ C)) is epsilon-transitive epsilon-connected ordinal set

(exp (D,(succ C))) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

succ (f +^ C) is epsilon-transitive epsilon-connected ordinal non empty set

{(f +^ C)} is non empty trivial 1 -element set

(f +^ C) \/ {(f +^ C)} is non empty set

exp (D,(succ (f +^ C))) is epsilon-transitive epsilon-connected ordinal set

D *^ (exp (D,(f +^ C))) is epsilon-transitive epsilon-connected ordinal set

D *^ (exp (D,C)) is epsilon-transitive epsilon-connected ordinal set

(D *^ (exp (D,C))) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

f +^ C is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ C)) is epsilon-transitive epsilon-connected ordinal set

exp (D,C) is epsilon-transitive epsilon-connected ordinal set

(exp (D,C)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

c is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom c is epsilon-transitive epsilon-connected ordinal set

b is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

e is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

c *^ (exp (D,f)) is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom (c *^ (exp (D,f))) is epsilon-transitive epsilon-connected ordinal set

(dom e) +^ e is epsilon-transitive epsilon-connected ordinal set

b . ((dom e) +^ e) is epsilon-transitive epsilon-connected ordinal set

f +^ e is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ e)) is epsilon-transitive epsilon-connected ordinal set

exp (D,e) is epsilon-transitive epsilon-connected ordinal set

(exp (D,e)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

c . e is epsilon-transitive epsilon-connected ordinal set

(c . e) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

(c *^ (exp (D,f))) . e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

b . e is epsilon-transitive epsilon-connected ordinal set

exp (D,e) is epsilon-transitive epsilon-connected ordinal set

e . e is epsilon-transitive epsilon-connected ordinal set

(dom e) +^ (dom (c *^ (exp (D,f)))) is epsilon-transitive epsilon-connected ordinal set

(e,(c *^ (exp (D,f)))) is Relation-like T-Sequence-like Function-like Ordinal-yielding set

lim b is epsilon-transitive epsilon-connected ordinal set

1 *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

f +^ {} is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ {})) is epsilon-transitive epsilon-connected ordinal set

(exp (D,{})) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp ((exp (D,f)),g) is epsilon-transitive epsilon-connected ordinal set

g *^ f is epsilon-transitive epsilon-connected ordinal set

exp (D,(g *^ f)) is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

exp ((exp (D,f)),C) is epsilon-transitive epsilon-connected ordinal set

C *^ f is epsilon-transitive epsilon-connected ordinal set

exp (D,(C *^ f)) is epsilon-transitive epsilon-connected ordinal set

succ C is epsilon-transitive epsilon-connected ordinal non empty set

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

exp ((exp (D,f)),(succ C)) is epsilon-transitive epsilon-connected ordinal set

(succ C) *^ f is epsilon-transitive epsilon-connected ordinal set

exp (D,((succ C) *^ f)) is epsilon-transitive epsilon-connected ordinal set

(exp (D,f)) *^ (exp (D,(C *^ f))) is epsilon-transitive epsilon-connected ordinal set

(C *^ f) +^ f is epsilon-transitive epsilon-connected ordinal set

exp (D,((C *^ f) +^ f)) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

exp ((exp (D,f)),C) is epsilon-transitive epsilon-connected ordinal set

C *^ f is epsilon-transitive epsilon-connected ordinal set

exp (D,(C *^ f)) is epsilon-transitive epsilon-connected ordinal set

c is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom c is epsilon-transitive epsilon-connected ordinal set

b is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

e is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom e is epsilon-transitive epsilon-connected ordinal set

rng b is set

e is set

b is set

b . b is set

e is epsilon-transitive epsilon-connected ordinal set

e *^ f is epsilon-transitive epsilon-connected ordinal set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

sup (dom e) is epsilon-transitive epsilon-connected ordinal set

e is set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e *^ f is epsilon-transitive epsilon-connected ordinal set

b . e is epsilon-transitive epsilon-connected ordinal set

b * e is Relation-like Function-like set

dom (b * e) is set

e is set

b is epsilon-transitive epsilon-connected ordinal set

b . b is epsilon-transitive epsilon-connected ordinal set

b *^ f is epsilon-transitive epsilon-connected ordinal set

e is set

b is epsilon-transitive epsilon-connected ordinal set

b . b is epsilon-transitive epsilon-connected ordinal set

b *^ f is epsilon-transitive epsilon-connected ordinal set

c . e is set

exp ((exp (D,f)),b) is epsilon-transitive epsilon-connected ordinal set

exp (D,(b *^ f)) is epsilon-transitive epsilon-connected ordinal set

e . (b . b) is epsilon-transitive epsilon-connected ordinal set

(b * e) . e is set

lim c is epsilon-transitive epsilon-connected ordinal set

C *^ {} is epsilon-transitive epsilon-connected ordinal set

exp ((exp (D,f)),{}) is epsilon-transitive epsilon-connected ordinal set

{} *^ f is epsilon-transitive epsilon-connected ordinal set

exp (D,({} *^ f)) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

exp (D,f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

exp (D,(succ g)) is epsilon-transitive epsilon-connected ordinal set

1 *^ (exp (D,g)) is epsilon-transitive epsilon-connected ordinal set

D *^ (exp (D,g)) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

exp (D,g) is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom C is epsilon-transitive epsilon-connected ordinal set

c is set

b is epsilon-transitive epsilon-connected ordinal set

C . b is epsilon-transitive epsilon-connected ordinal set

exp (D,b) is epsilon-transitive epsilon-connected ordinal set

rng C is set

sup C is epsilon-transitive epsilon-connected ordinal set

sup (rng C) is epsilon-transitive epsilon-connected ordinal set

lim C is epsilon-transitive epsilon-connected ordinal set

exp (D,{}) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

F

F

F

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

D . {} is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

F

f is epsilon-transitive epsilon-connected ordinal set

D . f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

D . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

f +^ C is epsilon-transitive epsilon-connected ordinal set

D . (f +^ C) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

f +^ C is epsilon-transitive epsilon-connected ordinal set

D . (f +^ C) is epsilon-transitive epsilon-connected ordinal set

succ C is epsilon-transitive epsilon-connected ordinal non empty set

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

f +^ (succ C) is epsilon-transitive epsilon-connected ordinal set

D . (f +^ (succ C)) is epsilon-transitive epsilon-connected ordinal set

succ (f +^ C) is epsilon-transitive epsilon-connected ordinal non empty set

{(f +^ C)} is non empty trivial 1 -element set

(f +^ C) \/ {(f +^ C)} is non empty set

c is epsilon-transitive epsilon-connected ordinal set

F

f +^ {} is epsilon-transitive epsilon-connected ordinal set

D . (f +^ {}) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

f +^ C is epsilon-transitive epsilon-connected ordinal set

sup D is epsilon-transitive epsilon-connected ordinal set

rng D is set

sup (rng D) is epsilon-transitive epsilon-connected ordinal set

f is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom f is epsilon-transitive epsilon-connected ordinal set

F

sup f is epsilon-transitive epsilon-connected ordinal set

rng f is set

sup (rng f) is epsilon-transitive epsilon-connected ordinal set

g is set

C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

b is set

f . b is set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

F

F

b is set

D . b is set

e is epsilon-transitive epsilon-connected ordinal set

succ e is epsilon-transitive epsilon-connected ordinal non empty set

{e} is non empty trivial 1 -element set

e \/ {e} is non empty set

D . (succ e) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

f . g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

f . C is epsilon-transitive epsilon-connected ordinal set

F

F

lim f is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal non empty set

[:(On D),(On D):] is set

bool [:(On D),(On D):] is set

f is Relation-like On D -defined On D -valued Function-like V25( On D, On D) Element of bool [:(On D),(On D):]

dom f is set

rng f is set

F

On F

[:(On F

bool [:(On F

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

rng D is set

f is set

g is set

D . g is set

C is epsilon-transitive epsilon-connected ordinal set

F

f is Relation-like On F

g is epsilon-transitive epsilon-connected ordinal Element of F

f . g is epsilon-transitive epsilon-connected ordinal set

F

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal non empty set

f is epsilon-transitive epsilon-connected ordinal Element of D

On D is epsilon-transitive epsilon-connected ordinal non empty set

f is epsilon-transitive epsilon-connected ordinal Element of D

On D is epsilon-transitive epsilon-connected ordinal non empty set

[:(On D),(On D):] is set

bool [:(On D),(On D):] is set

f is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]

g is epsilon-transitive epsilon-connected ordinal Element of D

f . g is epsilon-transitive epsilon-connected ordinal set

dom f is epsilon-transitive epsilon-connected ordinal set

rng f is set

C is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal non empty set

[:(On D),(On D):] is set

bool [:(On D),(On D):] is set

f is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]

g is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]

f * g is Relation-like Function-like set

rng f is set

dom f is epsilon-transitive epsilon-connected ordinal set

dom g is epsilon-transitive epsilon-connected ordinal set

dom (f * g) is set

rng g is set

rng (f * g) is set

C is Relation-like T-Sequence-like Function-like set

rng C is set

D is epsilon-transitive non empty V41() V42() universal set

(D) is epsilon-transitive epsilon-connected ordinal Element of D

f is epsilon-transitive non empty V41() V42() universal set

(f) is epsilon-transitive epsilon-connected ordinal non empty Element of f

D is epsilon-transitive non empty V41() V42() universal set

f is epsilon-transitive epsilon-connected ordinal Element of D

succ f is epsilon-transitive epsilon-connected ordinal non empty set

{f} is non empty trivial 1 -element set

f \/ {f} is non empty set

g is epsilon-transitive epsilon-connected ordinal Element of D

f +^ g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

f +^ C is epsilon-transitive epsilon-connected ordinal set

(D) is epsilon-transitive epsilon-connected ordinal non empty Element of D

{(D)} is non empty trivial 1 -element Element of D

[:C,{(D)}:] is set

(D) is epsilon-transitive epsilon-connected ordinal Element of D

{(D)} is non empty trivial 1 -element Element of D

[:f,{(D)}:] is Element of D

[:f,{(D)}:] \/ [:C,{(D)}:] is set

card ([:f,{(D)}:] \/ [:C,{(D)}:]) is epsilon-transitive epsilon-connected ordinal cardinal set

card D is epsilon-transitive epsilon-connected ordinal non empty cardinal set

c is set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

f +^ e is epsilon-transitive epsilon-connected ordinal set

card (f +^ C) is epsilon-transitive epsilon-connected ordinal cardinal set

D is epsilon-transitive non empty V41() V42() universal set

f is epsilon-transitive epsilon-connected ordinal Element of D

g is epsilon-transitive epsilon-connected ordinal Element of D

f *^ g is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

C *^ g is epsilon-transitive epsilon-connected ordinal set

[:C,g:] is set

card [:C,g:] is epsilon-transitive epsilon-connected ordinal cardinal set

card D is epsilon-transitive epsilon-connected ordinal non empty cardinal set

c is set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e *^ g is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

(e *^ g) +^ e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal Element of D

e is epsilon-transitive epsilon-connected ordinal Element of D

(D,b,e) is epsilon-transitive epsilon-connected ordinal Element of D

card (C *^ g) is epsilon-transitive epsilon-connected ordinal cardinal set

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal non empty set

[:(On D),(On D):] is set

bool [:(On D),(On D):] is set

f is epsilon-transitive epsilon-connected ordinal Element of D

g is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]

dom g is epsilon-transitive epsilon-connected ordinal set

D is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom D is epsilon-transitive epsilon-connected ordinal set

rng D is set

sup D is epsilon-transitive epsilon-connected ordinal set

sup (rng D) is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive non empty V41() V42() universal set

g is set

C is epsilon-transitive epsilon-connected ordinal set

union (rng D) is set

D .: (dom D) is set

g is epsilon-transitive epsilon-connected ordinal set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

{g} is non empty trivial 1 -element set

g \/ {g} is non empty set

C is set

c is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

card (dom D) is epsilon-transitive epsilon-connected ordinal cardinal set

card f is epsilon-transitive epsilon-connected ordinal non empty cardinal set

card (rng D) is epsilon-transitive epsilon-connected ordinal cardinal set

D is epsilon-transitive non empty V41() V42() universal set

On D is epsilon-transitive epsilon-connected ordinal non empty set

[:(On D),(On D):] is set

bool [:(On D),(On D):] is set

f is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]

dom f is epsilon-transitive epsilon-connected ordinal set

(D) is epsilon-transitive epsilon-connected ordinal Element of D

(D,f,(D)) is epsilon-transitive epsilon-connected ordinal Element of D

g is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like set

dom C is epsilon-transitive epsilon-connected ordinal set

C . {} is set

c is epsilon-transitive epsilon-connected ordinal set

C . c is set

succ c is epsilon-transitive epsilon-connected ordinal non empty set

{c} is non empty trivial 1 -element set

c \/ {c} is non empty set

C . (succ c) is set

b is epsilon-transitive epsilon-connected ordinal Element of D

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

c is epsilon-transitive epsilon-connected ordinal set

C . c is set

rng C is set

sup (rng C) is epsilon-transitive epsilon-connected ordinal set

c is set

b is set

C . b is set

e is epsilon-transitive epsilon-connected ordinal set

C . e is set

e is epsilon-transitive epsilon-connected ordinal Element of D

b is epsilon-transitive epsilon-connected ordinal Element of D

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

c is Relation-like T-Sequence-like Function-like Ordinal-yielding set

b is epsilon-transitive epsilon-connected ordinal set

dom c is epsilon-transitive epsilon-connected ordinal set

c . b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

c . e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

b +^ e is epsilon-transitive epsilon-connected ordinal set

c . (b +^ e) is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

b +^ e is epsilon-transitive epsilon-connected ordinal set

c . (b +^ e) is epsilon-transitive epsilon-connected ordinal set

succ e is epsilon-transitive epsilon-connected ordinal non empty set

{e} is non empty trivial 1 -element set

e \/ {e} is non empty set

b +^ (succ e) is epsilon-transitive epsilon-connected ordinal set

c . (b +^ (succ e)) is epsilon-transitive epsilon-connected ordinal set

succ (b +^ e) is epsilon-transitive epsilon-connected ordinal non empty set

{(b +^ e)} is non empty trivial 1 -element set

(b +^ e) \/ {(b +^ e)} is non empty set

b is epsilon-transitive epsilon-connected ordinal Element of D

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

b +^ {} is epsilon-transitive epsilon-connected ordinal set

c . (b +^ {}) is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

b +^ e is epsilon-transitive epsilon-connected ordinal set

sup c is epsilon-transitive epsilon-connected ordinal set

rng c is set

sup (rng c) is epsilon-transitive epsilon-connected ordinal set

b is set

dom c is epsilon-transitive epsilon-connected ordinal set

e is set

c . e is set

e is epsilon-transitive epsilon-connected ordinal set

c . e is epsilon-transitive epsilon-connected ordinal set

f | (sup c) is Relation-like rng f -valued T-Sequence-like Function-like Ordinal-yielding set

rng f is set

b is epsilon-transitive epsilon-connected ordinal Element of D

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

dom (f | (sup c)) is epsilon-transitive epsilon-connected ordinal set

sup (f | (sup c)) is epsilon-transitive epsilon-connected ordinal set

rng (f | (sup c)) is set

sup (rng (f | (sup c))) is epsilon-transitive epsilon-connected ordinal set

e is set

b is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

e is set

(f | (sup c)) . e is set

c is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal Element of D

f . c is epsilon-transitive epsilon-connected ordinal set

(D,f,u) is epsilon-transitive epsilon-connected ordinal Element of D

dom c is epsilon-transitive epsilon-connected ordinal set

z is set

c . z is set

z is epsilon-transitive epsilon-connected ordinal set

succ z is epsilon-transitive epsilon-connected ordinal non empty set

{z} is non empty trivial 1 -element set

z \/ {z} is non empty set

c . (succ z) is epsilon-transitive epsilon-connected ordinal set

f . u is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal set

(f | (sup c)) . e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(f | (sup c)) . b is epsilon-transitive epsilon-connected ordinal set

f . b is epsilon-transitive epsilon-connected ordinal set

f . e is epsilon-transitive epsilon-connected ordinal set

lim (f | (sup c)) is epsilon-transitive epsilon-connected ordinal set

f . (sup c) is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

C is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom C is epsilon-transitive epsilon-connected ordinal set

rng C is set

sup C is epsilon-transitive epsilon-connected ordinal set

sup (rng C) is epsilon-transitive epsilon-connected ordinal set

c is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom c is epsilon-transitive epsilon-connected ordinal set

rng c is set

sup c is epsilon-transitive epsilon-connected ordinal set

sup (rng c) is epsilon-transitive epsilon-connected ordinal set

c * C is Relation-like Function-like set

b is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

rng b is set

sup b is epsilon-transitive epsilon-connected ordinal set

sup (rng b) is epsilon-transitive epsilon-connected ordinal set

e is set

e is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

e is set

C . e is set

e is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

u is set

c . u is set

C . c is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal set

b . u is epsilon-transitive epsilon-connected ordinal set

C . e is epsilon-transitive epsilon-connected ordinal set

sup D is epsilon-transitive epsilon-connected ordinal set

D is epsilon-transitive epsilon-connected ordinal set

f is epsilon-transitive epsilon-connected ordinal set

g is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom g is epsilon-transitive epsilon-connected ordinal set

rng g is set

sup g is epsilon-transitive epsilon-connected ordinal set

sup (rng g) is epsilon-transitive epsilon-connected ordinal set

C is epsilon-transitive epsilon-connected ordinal set

g . C is epsilon-transitive epsilon-connected ordinal set

c is epsilon-transitive epsilon-connected ordinal set

succ c is epsilon-transitive epsilon-connected ordinal non empty set

{c} is non empty trivial 1 -element set

c \/ {c} is non empty set

b is epsilon-transitive epsilon-connected ordinal set

e is set

g . e is set

e is epsilon-transitive epsilon-connected ordinal set

succ C is epsilon-transitive epsilon-connected ordinal non empty set

{C} is non empty trivial 1 -element set

C \/ {C} is non empty set

D is epsilon-transitive epsilon-connected ordinal set

f is Relation-like D -valued T-Sequence-like Function-like Ordinal-yielding set

g is Relation-like D -valued T-Sequence-like Function-like Ordinal-yielding set

(f,g) is Relation-like T-Sequence-like Function-like Ordinal-yielding set

rng f is set

rng g is set

(rng f) \/ (rng g) is set

rng (f,g) is set