REAL is set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() Element of K19(REAL)
K19(REAL) is set
COMPLEX is set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() set
K19(NAT) is non empty V12() non finite set
K19(NAT) is non empty V12() non finite set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() Element of NAT
{{}} is functional non empty V12() finite finite-membered V35(1) set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set
rng a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V49() V53() set
the set is set
<% the set %> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set
a is Relation-like Function-like T-Sequence-like set
A is Relation-like Function-like non empty T-Sequence-like set
a ^ A is Relation-like Function-like T-Sequence-like set
dom a is epsilon-transitive epsilon-connected ordinal set
dom A is non empty epsilon-transitive epsilon-connected ordinal set
(dom a) +^ (dom A) is epsilon-transitive epsilon-connected ordinal set
dom (a ^ A) is epsilon-transitive epsilon-connected ordinal set
A ^ a is Relation-like Function-like T-Sequence-like set
dom A is non empty epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal set
(dom A) +^ (dom a) is epsilon-transitive epsilon-connected ordinal set
dom (A ^ a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a +^ A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like set
dom c3 is epsilon-transitive epsilon-connected ordinal set
c3 | a is Relation-like rng c3 -valued Function-like T-Sequence-like set
rng c3 is set
dom (c3 | a) is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like set
dom s is epsilon-transitive epsilon-connected ordinal set
(c3 | a) ^ s is Relation-like Function-like T-Sequence-like set
dom ((c3 | a) ^ s) is epsilon-transitive epsilon-connected ordinal set
A is set
B is epsilon-transitive epsilon-connected ordinal set
c3 . A is set
(c3 | a) . B is set
((c3 | a) ^ s) . A is set
B is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
a +^ c9 is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
a +^ c9 is epsilon-transitive epsilon-connected ordinal set
c3 . A is set
s . c9 is set
((c3 | a) ^ s) . A is set
B is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
rng a is set
A is Relation-like Function-like T-Sequence-like set
a ^ A is Relation-like Function-like T-Sequence-like set
rng (a ^ A) is set
rng A is set
dom (a ^ A) is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ (dom A) is epsilon-transitive epsilon-connected ordinal set
b is set
s is set
a . s is set
c is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . c is set
b is set
s is set
A . s is set
c is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ c is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . ((dom a) +^ c) is set
a is Relation-like Function-like T-Sequence-like set
A is Relation-like Function-like T-Sequence-like set
a ^ A is Relation-like Function-like T-Sequence-like set
rng (a ^ A) is set
c3 is epsilon-transitive epsilon-connected ordinal set
rng a is set
rng A is set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
dom a is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
dom a is epsilon-transitive epsilon-connected ordinal set
a .: NAT is set
a . 0 is set
c3 is set
b is set
a . b is set
s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
a . (succ s) is set
a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
A is epsilon-transitive epsilon-connected ordinal set
dom a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
a . A is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
A is epsilon-transitive epsilon-connected ordinal set
dom a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
a . A is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
a is epsilon-transitive epsilon-connected ordinal set
<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
rng <%a%> is non empty V12() finite V35(1) set
A is set
{a} is non empty V12() finite V35(1) set
a is epsilon-transitive epsilon-connected ordinal set
<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding V53() set
dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative Element of K19(NAT)
<%a%> . 0 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
<%a%> . b is epsilon-transitive epsilon-connected ordinal set
<%a%> . c3 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative set
<%a%> . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
<%a%> . b is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal set is epsilon-transitive epsilon-connected ordinal set
<% the epsilon-transitive epsilon-connected ordinal set %> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding () set
dom a is epsilon-transitive epsilon-connected ordinal set
Union a is epsilon-transitive epsilon-connected ordinal set
rng a is set
union (rng a) is set
the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal Element of dom a
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is set
a . s is set
c is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
a . c is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c3 *^ (exp (NAT,a)) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
exp (NAT,(succ a)) is epsilon-transitive epsilon-connected ordinal set
NAT *^ (exp (NAT,a)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
exp (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
exp (a,{}) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
exp (a,(succ c3)) is epsilon-transitive epsilon-connected ordinal set
a *^ (exp (a,c3)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
lim b is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
c is set
b . c is set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
b . A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
b . (succ A) is epsilon-transitive epsilon-connected ordinal set
exp (a,(succ A)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
exp (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
lim b is epsilon-transitive epsilon-connected ordinal set
s is set
b . s is set
c is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
exp (a,s) is epsilon-transitive epsilon-connected ordinal set
b . s is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last s is epsilon-transitive epsilon-connected ordinal set
dom s is epsilon-transitive epsilon-connected ordinal set
union (dom s) is epsilon-transitive epsilon-connected ordinal set
s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set
s . {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c is epsilon-transitive epsilon-connected ordinal set
dom c is epsilon-transitive epsilon-connected ordinal set
union (dom c) is epsilon-transitive epsilon-connected ordinal set
c . (union (dom c)) is epsilon-transitive epsilon-connected ordinal set
c . {} is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
B is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last B is epsilon-transitive epsilon-connected ordinal set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c is epsilon-transitive epsilon-connected ordinal set
dom c is epsilon-transitive epsilon-connected ordinal set
union (dom c) is epsilon-transitive epsilon-connected ordinal set
c . (union (dom c)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
c . {} is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
(a,{}) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
(a,(succ A)) is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,A)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
A . {} is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A,a) is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(A,b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
B is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last B is epsilon-transitive epsilon-connected ordinal set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
succ c is non empty epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
(A,c) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,0) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,0)) is epsilon-transitive epsilon-connected ordinal set
exp (a,1) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(1,a) is epsilon-transitive epsilon-connected ordinal set
(1,{}) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(1,A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
(1,(succ A)) is epsilon-transitive epsilon-connected ordinal set
exp (1,1) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(1,A) is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
{1} is non empty V12() finite finite-membered V35(1) set
b is set
s is set
c3 . s is set
c is epsilon-transitive epsilon-connected ordinal set
(1,c) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of A is epsilon-transitive epsilon-connected ordinal Element of A
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
c3 . c9 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,2) is epsilon-transitive epsilon-connected ordinal set
exp (a,a) is epsilon-transitive epsilon-connected ordinal set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,1) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,1)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,3) is epsilon-transitive epsilon-connected ordinal set
exp (a,a) is epsilon-transitive epsilon-connected ordinal set
exp (a,(exp (a,a))) is epsilon-transitive epsilon-connected ordinal set
succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,2) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,2)) is epsilon-transitive epsilon-connected ordinal set
2 * 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding increasing V53() () () () Element of NAT
(0,(2 * 0)) is epsilon-transitive epsilon-connected ordinal set
(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,((2 * 0) + 1)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
2 * a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(0,(2 * a)) is epsilon-transitive epsilon-connected ordinal set
(2 * a) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,((2 * a) + 1)) is epsilon-transitive epsilon-connected ordinal set
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
2 * (a + 1) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(0,(2 * (a + 1))) is epsilon-transitive epsilon-connected ordinal set
(2 * (a + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,((2 * (a + 1)) + 1)) is epsilon-transitive epsilon-connected ordinal set
((2 * a) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,(((2 * a) + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set
succ ((2 * a) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(0,(succ ((2 * a) + 1))) is epsilon-transitive epsilon-connected ordinal set
exp (0,0) is epsilon-transitive epsilon-connected ordinal set
succ (2 * (a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(0,(succ (2 * (a + 1)))) is epsilon-transitive epsilon-connected ordinal set
exp (0,1) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(c3,a) is epsilon-transitive epsilon-connected ordinal set
(c3,A) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
b is epsilon-transitive epsilon-connected ordinal set
(c3,b) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
(c3,s) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
(c3,(succ b)) is epsilon-transitive epsilon-connected ordinal set
(c3,b) is epsilon-transitive epsilon-connected ordinal set
exp (c3,(c3,b)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
(c3,s) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
(c3,c) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
s . c is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
s . A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
(c3,B) is epsilon-transitive epsilon-connected ordinal set
(c3,c9) is epsilon-transitive epsilon-connected ordinal set
(c3,c) is epsilon-transitive epsilon-connected ordinal set
(c3,A) is epsilon-transitive epsilon-connected ordinal set
Union s is epsilon-transitive epsilon-connected ordinal set
rng s is set
union (rng s) is set
(c3,b) is epsilon-transitive epsilon-connected ordinal set
lim s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
(c3,c) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(c3,A) is epsilon-transitive epsilon-connected ordinal set
s . c is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
(a,(succ c3)) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,c3)) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
exp (a,1) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
b . s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b . c is epsilon-transitive epsilon-connected ordinal set
(a,c) is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
lim b is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
b . 1 is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(A + 1) + b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,0) is epsilon-transitive epsilon-connected ordinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(0 + 1)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,s) is epsilon-transitive epsilon-connected ordinal set
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(s + 1)) is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ (s + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
exp (a,(a,s)) is epsilon-transitive epsilon-connected ordinal set
(a,((s + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,(s + 1))) is epsilon-transitive epsilon-connected ordinal set
(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((s + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set
(A + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((A + 1) + 0)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(A + 1) + s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((A + 1) + s)) is epsilon-transitive epsilon-connected ordinal set
((A + 1) + s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(((A + 1) + s) + 1)) is epsilon-transitive epsilon-connected ordinal set
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(A + 1) + (s + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((A + 1) + (s + 1))) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . s is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . c is epsilon-transitive epsilon-connected ordinal set
(a,c) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,1) is epsilon-transitive epsilon-connected ordinal set
(a,2) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,0) is epsilon-transitive epsilon-connected ordinal set
a |^ 0 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
a |^ A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
exp (a,(A + 1)) is epsilon-transitive epsilon-connected ordinal set
a *^ (exp (a,A)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
c3 * b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
a |^ (A + 1) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
a |^ A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,A) is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
c3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,b) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,A) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,0) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,c3) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,(a,c3)) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a |^ (a,c3) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a |^ c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
rng A is set
c3 is set
b is set
A . b is set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(a,s) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
lim A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(a,s) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(a,B) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A . B is epsilon-transitive epsilon-connected ordinal set
A . A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . s is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
(a,c) is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
sup A is epsilon-transitive epsilon-connected ordinal set
rng A is set
sup (rng A) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,NAT)) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
lim A is epsilon-transitive epsilon-connected ordinal set
Union A is epsilon-transitive epsilon-connected ordinal set
rng A is set
union (rng A) is set
b is set
s is set
c3 . s is set
c is set
A . c is set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . B is epsilon-transitive epsilon-connected ordinal set
exp (a,(A . B)) is epsilon-transitive epsilon-connected ordinal set
succ B is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 . A is epsilon-transitive epsilon-connected ordinal set
(a,B) is epsilon-transitive epsilon-connected ordinal set
A . (succ B) is epsilon-transitive epsilon-connected ordinal set
(a,(succ B)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
A -^ NAT is epsilon-transitive epsilon-connected ordinal set
NAT +^ (A -^ NAT) is epsilon-transitive epsilon-connected ordinal set
NAT +^ {} is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ {})) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
NAT +^ c3 is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ c3)) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
NAT +^ (succ c3) is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ (succ c3))) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,(NAT +^ c3))) is epsilon-transitive epsilon-connected ordinal set
succ (NAT +^ c3) is non empty epsilon-transitive epsilon-connected ordinal set
(a,(succ (NAT +^ c3))) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
NAT +^ c3 is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ c3)) is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
lim b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() set
B is epsilon-transitive epsilon-connected ordinal set
B -^ A is epsilon-transitive epsilon-connected ordinal set
(NAT +^ c3) -^ NAT is epsilon-transitive epsilon-connected ordinal set
NAT +^ (B -^ A) is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ (B -^ A))) is epsilon-transitive epsilon-connected ordinal set
(a,B) is epsilon-transitive epsilon-connected ordinal set
b . B is epsilon-transitive epsilon-connected ordinal set
F2() is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom F2() is epsilon-transitive epsilon-connected ordinal set
F2() . 0 is epsilon-transitive epsilon-connected ordinal set
F1() is epsilon-transitive epsilon-connected ordinal set
Union F2() is epsilon-transitive epsilon-connected ordinal set
rng F2() is set
union (rng F2()) is set
F3((Union F2())) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
F3(A) is epsilon-transitive epsilon-connected ordinal set
F3(F3(A)) is epsilon-transitive epsilon-connected ordinal set
F3(F1()) is epsilon-transitive epsilon-connected ordinal set
A is set
F2() . A is set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
F2() . b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ b) is epsilon-transitive epsilon-connected ordinal set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
F2() . (b + 1) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . c3 is epsilon-transitive epsilon-connected ordinal set
{F1()} is non empty V12() finite V35(1) set
A is set
c3 is set
F2() . c3 is set
A is epsilon-transitive epsilon-connected ordinal set
F3(A) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
F2() . (succ A) is epsilon-transitive epsilon-connected ordinal set
F2() . A is epsilon-transitive epsilon-connected ordinal set
F3((F2() . A)) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
F2() . A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
F2() . (succ A) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ 0) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
F2() . b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ b) is epsilon-transitive epsilon-connected ordinal set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ (b + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (b + 1) is epsilon-transitive epsilon-connected ordinal set
F3((F2() . b)) is epsilon-transitive epsilon-connected ordinal set
F2() . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set
F3((F2() . (b + 1))) is epsilon-transitive epsilon-connected ordinal set
F2() . (succ (b + 1)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . c3 is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ c3) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . 1 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is set
F2() . b is set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ s) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
F3(c3) is epsilon-transitive epsilon-connected ordinal set
F3(b) is epsilon-transitive epsilon-connected ordinal set
sup A is epsilon-transitive epsilon-connected ordinal set
rng A is set
sup (rng A) is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
c3 is set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is set
A . c is set
A is epsilon-transitive epsilon-connected ordinal set
B is set
F2() . B is set
c9 is epsilon-transitive epsilon-connected ordinal set
F2() . c9 is epsilon-transitive epsilon-connected ordinal set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal set
F2() . (succ c9) is epsilon-transitive epsilon-connected ordinal set
F3((F2() . c9)) is epsilon-transitive epsilon-connected ordinal set
F3(A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
F3(c3) is epsilon-transitive epsilon-connected ordinal set
b is set
s is set
F2() . s is set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
F2() . A is epsilon-transitive epsilon-connected ordinal set
F3((F2() . A)) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ A) is epsilon-transitive epsilon-connected ordinal set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
F2() . (A + 1) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . c is epsilon-transitive epsilon-connected ordinal set
union c3 is epsilon-transitive epsilon-connected ordinal set
F1() is epsilon-transitive epsilon-connected ordinal set
succ F1() is non empty epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
a . {} is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
F2(A) is epsilon-transitive epsilon-connected ordinal set
F2(F2(A)) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
F2(A) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
a . 0 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a . b is epsilon-transitive epsilon-connected ordinal set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
a . (b + 1) is epsilon-transitive epsilon-connected ordinal set
F2((a . b)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
a . c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
A +^ {} is epsilon-transitive epsilon-connected ordinal set
a . (A +^ {}) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A +^ b is epsilon-transitive epsilon-connected ordinal set
a . (A +^ b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
A +^ (succ b) is epsilon-transitive epsilon-connected ordinal set
a . (A +^ (succ b)) is epsilon-transitive epsilon-connected ordinal set
succ (A +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
F2(s) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A +^ b is epsilon-transitive epsilon-connected ordinal set
a . (A +^ b) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A +^ b is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
F2((sup a)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
F2(c3) is epsilon-transitive epsilon-connected ordinal set
F2(b) is epsilon-transitive epsilon-connected ordinal set
sup A is epsilon-transitive epsilon-connected ordinal set
rng A is set
sup (rng A) is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
c3 is set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is set
A . c is set
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
c9 is set
a . c9 is set
c is epsilon-transitive epsilon-connected ordinal set
succ c is non empty epsilon-transitive epsilon-connected ordinal set
a . (succ c) is epsilon-transitive epsilon-connected ordinal set
F2(B) is epsilon-transitive epsilon-connected ordinal set
F2(A) is epsilon-transitive epsilon-connected ordinal set
a . 0 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c3 . b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c3 . s is epsilon-transitive epsilon-connected ordinal set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,s) is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal () set
b is epsilon-transitive epsilon-connected ordinal () set
A is epsilon-transitive epsilon-connected ordinal () set
c3 is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal () set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal () set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal () set
c3 is epsilon-transitive epsilon-connected ordinal () set
(0) is epsilon-transitive epsilon-connected ordinal () set
(NAT,NAT) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
Union A is epsilon-transitive epsilon-connected ordinal set
rng A is set
union (rng A) is set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
a . {} is epsilon-transitive epsilon-connected ordinal set
a . 0 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
a . (succ A) is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(a . A)) is epsilon-transitive epsilon-connected ordinal set
Union a is epsilon-transitive epsilon-connected ordinal set
rng a is set
union (rng a) is set
exp (NAT,(Union a)) is epsilon-transitive epsilon-connected ordinal set
(NAT,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a . c3 is epsilon-transitive epsilon-connected ordinal set
(NAT,c3) is epsilon-transitive epsilon-connected ordinal set
c3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
a . (c3 + 1) is epsilon-transitive epsilon-connected ordinal set
(NAT,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
exp (NAT,(a . c3)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
(NAT,c3) is epsilon-transitive epsilon-connected ordinal set
lim a is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . b is epsilon-transitive epsilon-connected ordinal set
(NAT,c3) is epsilon-transitive epsilon-connected ordinal set
(NAT,b) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
a . s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(NAT,c) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal () set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 is epsilon-transitive epsilon-connected ordinal () set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal () set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,0) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,1) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
a is epsilon-transitive epsilon-connected ordinal set
exp (NAT,0) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
a is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
exp (a,NAT) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
exp (a,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
1 +^ NAT is epsilon-transitive epsilon-connected ordinal set
exp (a,(1 +^ NAT)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (a,(1 +^ NAT)))) is epsilon-transitive epsilon-connected ordinal set
exp (a,1) is epsilon-transitive epsilon-connected ordinal set
(exp (a,NAT)) *^ (exp (a,1)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (a,NAT)) *^ (exp (a,1)))) is epsilon-transitive epsilon-connected ordinal set
(exp (a,NAT)) *^ a is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (a,NAT)) *^ a)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
exp ((exp (NAT,a)),(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
(A,(a + 2)) is epsilon-transitive epsilon-connected ordinal set
(A,(a + 1)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set
(A,a) is epsilon-transitive epsilon-connected ordinal set
(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(A,((a + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set
succ (a + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(A,(succ (a + 1))) is epsilon-transitive epsilon-connected ordinal set
exp (A,(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
exp ((exp (NAT,A)),(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set
(A,(a + 1)) *^ A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((A,(a + 1)) *^ A)) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(A,(succ a)) is epsilon-transitive epsilon-connected ordinal set
(A,(succ a)) *^ A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((A,(succ a)) *^ A)) is epsilon-transitive epsilon-connected ordinal set
exp (A,(A,a)) is epsilon-transitive epsilon-connected ordinal set
(exp (A,(A,a))) *^ A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (A,(A,a))) *^ A)) is epsilon-transitive epsilon-connected ordinal set
exp (A,1) is epsilon-transitive epsilon-connected ordinal set
(exp (A,(A,a))) *^ (exp (A,1)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (A,(A,a))) *^ (exp (A,1)))) is epsilon-transitive epsilon-connected ordinal set
1 +^ (A,a) is epsilon-transitive epsilon-connected ordinal set
exp (A,(1 +^ (A,a))) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (A,(1 +^ (A,a))))) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (A,(A,a)))) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A,(succ a))) is epsilon-transitive epsilon-connected ordinal set
a is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
(a) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c3 . b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c3 . s is epsilon-transitive epsilon-connected ordinal set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,s) is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
A . {} is epsilon-transitive epsilon-connected ordinal set
A . 0 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
A . (succ c3) is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A . c3)) is epsilon-transitive epsilon-connected ordinal set
Union A is epsilon-transitive epsilon-connected ordinal set
rng A is set
union (rng A) is set
exp (NAT,(Union A)) is epsilon-transitive epsilon-connected ordinal set
c3 is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
b is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A . 1 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(succ a)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
NAT *^ H1(a) is epsilon-transitive epsilon-connected ordinal set
NAT *^ a is epsilon-transitive epsilon-connected ordinal set
A . 2 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(NAT *^ a)) is epsilon-transitive epsilon-connected ordinal set
exp (H1(a),NAT) is epsilon-transitive epsilon-connected ordinal set
exp (a,NAT) is epsilon-transitive epsilon-connected ordinal set
A . 3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
exp (a,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
(a,2) is epsilon-transitive epsilon-connected ordinal set
exp (a,a) is epsilon-transitive epsilon-connected ordinal set
exp (a,1) is epsilon-transitive epsilon-connected ordinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A . (0 + 1) is epsilon-transitive epsilon-connected ordinal set
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(0 + 2)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,b) is epsilon-transitive epsilon-connected ordinal set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A . (b + 1) is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
b + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(b + 2)) is epsilon-transitive epsilon-connected ordinal set
(a,(b + 1)) is epsilon-transitive epsilon-connected ordinal set
(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set
(b + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((b + 1) + 2)) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ (b + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
exp (NAT,(A . b)) is epsilon-transitive epsilon-connected ordinal set
A . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A . (b + 1))) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
2 + s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
s + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(s + 2)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(a,(s + 2))) is epsilon-transitive epsilon-connected ordinal set
(s + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((s + 1) + 2)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(a,(b + 2))) is epsilon-transitive epsilon-connected ordinal set
(b + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((b + 1) + 2)) is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
lim b is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
s is set
c is set
A . c is set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . A is epsilon-transitive epsilon-connected ordinal set
A + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(A + 2)) is epsilon-transitive epsilon-connected ordinal set
b . (A + 2) is epsilon-transitive epsilon-connected ordinal set
s is set
c is set
b . c is set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,A) is epsilon-transitive epsilon-connected ordinal set
A . (A + 1) is epsilon-transitive epsilon-connected ordinal set
b . A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last b is epsilon-transitive epsilon-connected ordinal set
dom b is epsilon-transitive epsilon-connected ordinal set
union (dom b) is epsilon-transitive epsilon-connected ordinal set
b . (union (dom b)) is epsilon-transitive epsilon-connected ordinal set
b . {} is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last s is epsilon-transitive epsilon-connected ordinal set
dom s is epsilon-transitive epsilon-connected ordinal set
union (dom s) is epsilon-transitive epsilon-connected ordinal set
s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set
s . {} is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
A . {} is epsilon-transitive epsilon-connected ordinal set
(0) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last s is epsilon-transitive epsilon-connected ordinal set
dom s is epsilon-transitive epsilon-connected ordinal set
union (dom s) is epsilon-transitive epsilon-connected ordinal set
s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
s . {} is epsilon-transitive epsilon-connected ordinal set
(c3) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
((succ a)) is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
((a),NAT) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c is epsilon-transitive epsilon-connected ordinal set
dom c is epsilon-transitive epsilon-connected ordinal set
union (dom c) is epsilon-transitive epsilon-connected ordinal set
c . (union (dom c)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
c . {} is epsilon-transitive epsilon-connected ordinal set
(b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
A . {} is epsilon-transitive epsilon-connected ordinal set
(s) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(c3) is epsilon-transitive epsilon-connected ordinal set
(b) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
((succ c3)) is epsilon-transitive epsilon-connected ordinal set
((c3),NAT) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
(s) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(c3) is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
b . s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b . c is epsilon-transitive epsilon-connected ordinal set
(s) is epsilon-transitive epsilon-connected ordinal set
(c) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
(B) is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
lim b is epsilon-transitive epsilon-connected ordinal set
b . 0 is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
(s) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
(c) is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
((succ s)) is epsilon-transitive epsilon-connected ordinal set
b . (succ s) is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
(c3) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
Union A is epsilon-transitive epsilon-connected ordinal set
rng A is set
union (rng A) is set
lim A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
A is set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
b is set
c3 . b is set
s 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
c3 . b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
((succ A)) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
c3 is set
b is epsilon-transitive epsilon-connected ordinal set
(b) is epsilon-transitive epsilon-connected ordinal set
a is non empty set
union a is set
A is set
c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
b is set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
s is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
the Element of a is Element of a
b is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
b is set
s is epsilon-transitive epsilon-connected ordinal set
exp (NAT,s) is epsilon-transitive epsilon-connected ordinal set
c is set
A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
a is non empty set
union a is set
A is set
c3 is epsilon-transitive epsilon-connected ordinal set
(c3) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
b is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
({}) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
((succ A)) is epsilon-transitive epsilon-connected ordinal set
((A)) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
((A),NAT) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
c3 . 0 is epsilon-transitive epsilon-connected ordinal set
c is set
s is non empty set
A is set
c3 . A is set
B is epsilon-transitive epsilon-connected ordinal set
(B) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is set
c3 . A is set
B is epsilon-transitive epsilon-connected ordinal set
succ B is non empty epsilon-transitive epsilon-connected ordinal set
c9 is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
(B) is epsilon-transitive epsilon-connected ordinal set
(c9) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
(H1(B),NAT) is epsilon-transitive epsilon-connected ordinal set
((succ B)) is epsilon-transitive epsilon-connected ordinal set
c3 . (succ B) is epsilon-transitive epsilon-connected ordinal set
(c) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
a is epsilon-transitive epsilon-connected ordinal set
({}) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
A is epsilon-transitive epsilon-connected ordinal set
(A) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
((succ A)) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
c3 is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
((A),NAT) is epsilon-transitive epsilon-connected ordinal set
((A)) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
A is epsilon-transitive epsilon-connected ordinal set
(A) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
c3 is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
b is epsilon-transitive epsilon-connected ordinal set
(b) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
(a) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
((succ a)) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
a is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
dom a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of K19(NAT)
succ (dom a) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last b is epsilon-transitive epsilon-connected ordinal set
dom b is epsilon-transitive epsilon-connected ordinal set
union (dom b) is epsilon-transitive epsilon-connected ordinal set
b . (union (dom b)) is epsilon-transitive epsilon-connected ordinal set
b . {} is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last b is epsilon-transitive epsilon-connected ordinal set
dom b is epsilon-transitive epsilon-connected ordinal set
union (dom b) is epsilon-transitive epsilon-connected ordinal set
b . (union (dom b)) is epsilon-transitive epsilon-connected ordinal set
b . 0 is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c is epsilon-transitive epsilon-connected ordinal set
dom c is epsilon-transitive epsilon-connected ordinal set
union (dom c) is epsilon-transitive epsilon-connected ordinal set
c . (union (dom c)) is epsilon-transitive epsilon-connected ordinal set
c . 0 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
succ A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
c . (A + 1) is epsilon-transitive epsilon-connected ordinal set
c . A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
(c . A) +^ (a . A) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
A . 0 is epsilon-transitive epsilon-connected ordinal set
B is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last B is epsilon-transitive epsilon-connected ordinal set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
B . 0 is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c is epsilon-transitive epsilon-connected ordinal set
succ c is non empty epsilon-transitive epsilon-connected ordinal set
A . (succ c) is epsilon-transitive epsilon-connected ordinal set
A . c is epsilon-transitive epsilon-connected ordinal set
a . c is epsilon-transitive epsilon-connected ordinal set
(A . c) +^ (a . c) is epsilon-transitive epsilon-connected ordinal set
c11 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
c11 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A . (c11 + 1) is epsilon-transitive epsilon-connected ordinal set
A . c11 is epsilon-transitive epsilon-connected ordinal set
a . c11 is epsilon-transitive epsilon-connected ordinal set
(A . c11) +^ (a . c11) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A . c is epsilon-transitive epsilon-connected ordinal set
A | c is Relation-like rng A -valued Function-like T-Sequence-like Ordinal-yielding set
rng A is set
Union (A | c) is epsilon-transitive epsilon-connected ordinal set
rng (A | c) is set
union (rng (A | c)) is set
c is epsilon-transitive epsilon-connected ordinal set
succ c is non empty epsilon-transitive epsilon-connected ordinal set
B . (succ c) is epsilon-transitive epsilon-connected ordinal set
B . c is epsilon-transitive epsilon-connected ordinal set
a . c is epsilon-transitive epsilon-connected ordinal set
(B . c) +^ (a . c) is epsilon-transitive epsilon-connected ordinal set
c11 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
c11 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
B . (c11 + 1) is epsilon-transitive epsilon-connected ordinal set
B . c11 is epsilon-transitive epsilon-connected ordinal set
a . c11 is epsilon-transitive epsilon-connected ordinal set
(B . c11) +^ (a . c11) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
B . c is epsilon-transitive epsilon-connected ordinal set
B | c is Relation-like rng B -valued Function-like T-Sequence-like Ordinal-yielding set
rng B is set
Union (B | c) is epsilon-transitive epsilon-connected ordinal set
rng (B | c) is set
union (rng (B | c)) is set
c is epsilon-transitive epsilon-connected ordinal set
c11 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c11 is epsilon-transitive epsilon-connected ordinal set
dom c11 is epsilon-transitive epsilon-connected ordinal set
union (dom c11) is epsilon-transitive epsilon-connected ordinal set
c11 . (union (dom c11)) is epsilon-transitive epsilon-connected ordinal set
c11 . {} is epsilon-transitive epsilon-connected ordinal set
({}) is epsilon-transitive epsilon-connected ordinal set
a is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
(a) is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of K19(NAT)
succ (dom a) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
A . 0 is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
a is epsilon-transitive epsilon-connected ordinal set
<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
(<%a%>) is epsilon-transitive epsilon-connected ordinal set
dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative Element of K19(NAT)
succ (dom <%a%>) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
A . 0 is epsilon-transitive epsilon-connected ordinal set
<%a%> . 0 is epsilon-transitive epsilon-connected ordinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A . (0 + 1) is epsilon-transitive epsilon-connected ordinal set
0 +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
A is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
A ^ <%a%> is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
((A ^ <%a%>)) is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
(A) +^ a is epsilon-transitive epsilon-connected ordinal set
dom (A ^ <%a%>) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of K19(NAT)
succ (dom (A ^ <%a%>)) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c3 is epsilon-transitive epsilon-connected ordinal set
dom c3 is epsilon-transitive epsilon-connected ordinal set
union (dom c3) is epsilon-transitive epsilon-connected ordinal set
c3 . (union (dom c3)) is epsilon-transitive epsilon-connected ordinal set
c3 . 0 is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of K19(NAT)
succ (dom A) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last b is epsilon-transitive epsilon-connected ordinal set
dom b is epsilon-transitive epsilon-connected ordinal set
union (dom b) is epsilon-transitive epsilon-connected ordinal set
b . (union (dom b)) is epsilon-transitive epsilon-connected ordinal set
b . 0 is epsilon-transitive epsilon-connected ordinal set
dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative Element of K19(NAT)
(dom A) +^ 1 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c3 . c is epsilon-transitive epsilon-connected ordinal set
b . c is epsilon-transitive epsilon-connected ordinal set
c + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
c3 . (c + 1) is epsilon-transitive epsilon-connected ordinal set
b . (c + 1) is epsilon-transitive epsilon-connected ordinal set
succ c is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A . c is epsilon-transitive epsilon-connected ordinal set
(b . c) +^ (A . c) is epsilon-transitive epsilon-connected ordinal set
(A ^ <%a%>) . c is epsilon-transitive epsilon-connected ordinal set
(c3 . c) +^ ((A ^ <%a%>) . c) is epsilon-transitive epsilon-connected ordinal set
c3 . ((dom A) +^ 1) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
c3 . (s + 1) is epsilon-transitive epsilon-connected ordinal set
c3 . (dom A) is epsilon-transitive epsilon-connected ordinal set
len A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
dom A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(A ^ <%a%>) . (len A) is epsilon-transitive epsilon-connected ordinal set
(c3 . (dom A)) +^ ((A ^ <%a%>) . (len A)) is epsilon-transitive epsilon-connected ordinal set
(c3 . (dom A)) +^ a is epsilon-transitive epsilon-connected ordinal set
b . (dom A) is epsilon-transitive epsilon-connected ordinal set
(b . (dom A)) +^ a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
<%a%> ^ {} is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
((<%a%> ^ {})) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
<%a%> ^ A is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
((<%a%> ^ A)) is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
a +^ (A) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like T-Sequence-like finite V53() set
c3 is set
<%c3%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set
A ^ <%c3%> is Relation-like NAT -defined Function-like non empty T-Sequence-like finite V53() set
b is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
<%a%> ^ b is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
((<%a%> ^ b)) is epsilon-transitive epsilon-connected ordinal set
(b) is epsilon-transitive epsilon-connected ordinal set
a +^ (b) is epsilon-transitive epsilon-connected ordinal set
rng b is finite set
s is epsilon-transitive epsilon-connected ordinal set
rng A is finite set
rng <%c3%> is non empty V12() finite V35(1) set
(rng A) \/ (rng <%c3%>) is non empty finite set
{c3} is non empty V12() finite V35(1) set
c is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
<%a%> ^ c is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
A is epsilon-transitive epsilon-connected ordinal set
<%A%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
(<%a%> ^ c) ^ <%A%> is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
(((<%a%> ^ c) ^ <%A%>)) is epsilon-transitive epsilon-connected ordinal set
((<%a%> ^ c)) is epsilon-transitive epsilon-connected ordinal set
((<%a%> ^ c)) +^ A is epsilon-transitive epsilon-connected ordinal set
(c) is epsilon-transitive epsilon-connected ordinal set
a +^ (c) is epsilon-transitive epsilon-connected ordinal set
(a +^ (c)) +^ A is epsilon-transitive epsilon-connected ordinal set
(c) +^ A is epsilon-transitive epsilon-connected ordinal set
a +^ ((c) +^ A) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
<%a%> ^ A is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
((<%a%> ^ A)) is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
a +^ (A) is epsilon-transitive epsilon-connected ordinal set
a is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
a . 0 is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
A . 0 is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like T-Sequence-like finite V53() set
c3 is set
<%c3%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set
A ^ <%c3%> is Relation-like NAT -defined Function-like non empty T-Sequence-like finite V53() set
b is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
b . 0 is epsilon-transitive epsilon-connected ordinal set
(b) is epsilon-transitive epsilon-connected ordinal set
rng b is finite set
s is epsilon-transitive epsilon-connected ordinal set
rng A is finite set
rng <%c3%> is non empty V12() finite V35(1) set
(rng A) \/ (rng <%c3%>) is non empty finite set
{c3} is non empty V12() finite V35(1) set
A is epsilon-transitive epsilon-connected ordinal set
<%A%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
{} ^ <%A%> is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
c is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() set
dom c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of K19(NAT)
(c) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(c) +^ A is epsilon-transitive epsilon-connected ordinal set
c . 0 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
c3 *^ (exp (NAT,A)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,1) is epsilon-transitive epsilon-connected ordinal set
1 *^ (exp (NAT,1)) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
exp (A,a) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (A,c3) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
exp (A,b) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
exp (A,s) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
exp (A,0) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
exp (A,b) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
exp (A,s) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
exp (A,c) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (A,c3) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
exp (A,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A,a) is epsilon-transitive epsilon-connected ordinal set
succ (A,a) is non empty epsilon-transitive epsilon-connected ordinal set
exp (a,(succ (A,a))) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c3 *^ (exp (a,A)) is epsilon-transitive epsilon-connected ordinal set
((c3 *^ (exp (a,A))),a) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
1 *^ (exp (a,A)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
exp (a,b) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
exp (a,(succ A)) is epsilon-transitive epsilon-connected ordinal set
a *^ (exp (a,A)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (A,c3) is epsilon-transitive epsilon-connected ordinal set
a div^ (exp (A,c3)) is epsilon-transitive epsilon-connected ordinal set
(a div^ (exp (A,c3))) *^ (exp (A,c3)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
((a div^ (exp (A,c3))) *^ (exp (A,c3))) +^ s is epsilon-transitive epsilon-connected ordinal set
A *^ (exp (A,c3)) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
exp (A,(succ c3)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (A,c3) is epsilon-transitive epsilon-connected ordinal set
a div^ (exp (A,c3)) is epsilon-transitive epsilon-connected ordinal set
(a div^ (exp (A,c3))) *^ (exp (A,c3)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
((a div^ (exp (A,c3))) *^ (exp (A,c3))) +^ s is epsilon-transitive epsilon-connected ordinal set
0 +^ s is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
A mod^ (exp (a,c3)) is epsilon-transitive epsilon-connected ordinal set
A div^ (exp (a,c3)) is epsilon-transitive epsilon-connected ordinal set
(A div^ (exp (a,c3))) *^ (exp (a,c3)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
((A div^ (exp (a,c3))) *^ (exp (a,c3))) +^ s is epsilon-transitive epsilon-connected ordinal set
A -^ ((A div^ (exp (a,c3))) *^ (exp (a,c3))) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(a,NAT)) is epsilon-transitive epsilon-connected ordinal set
a div^ (exp (NAT,(a,NAT))) is epsilon-transitive epsilon-connected ordinal set
a mod^ (exp (NAT,(a,NAT))) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
s *^ (exp (NAT,(a,NAT))) is epsilon-transitive epsilon-connected ordinal set
(s *^ (exp (NAT,(a,NAT)))) +^ (a mod^ (exp (NAT,(a,NAT)))) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A,a) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(c3,a) is epsilon-transitive epsilon-connected ordinal set
succ (A,a) is non empty epsilon-transitive epsilon-connected ordinal set
exp (a,(succ (A,a))) is epsilon-transitive epsilon-connected ordinal set
exp (a,(c3,a)) is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
((a . c3),NAT) is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
((a . A),NAT) is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
((a . c3),NAT) is epsilon-transitive epsilon-connected ordinal set
((a . A),NAT) is epsilon-transitive epsilon-connected ordinal set
a is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() () () () set
(a) is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of K19(NAT)
a . 0 is epsilon-transitive epsilon-connected ordinal set
A is non empty epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A *^ (exp (NAT,a)) is epsilon-transitive epsilon-connected ordinal set
<%(A *^ (exp (NAT,a)))%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
dom <%(A *^ (exp (NAT,a)))%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative Element of K19(NAT)
<%(A *^ (exp (NAT,a)))%> . 0 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
<%(A *^ (exp (NAT,a)))%> . b is epsilon-transitive epsilon-connected ordinal set
dom <%(A *^ (exp (NAT,a)))%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative set
b is epsilon-transitive epsilon-connected ordinal set
<%(A *^ (exp (NAT,a)))%> . b is epsilon-transitive epsilon-connected ordinal set
((<%(A *^ (exp (NAT,a)))%> . b),NAT) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
<%(A *^ (exp (NAT,a)))%> . s is epsilon-transitive epsilon-connected ordinal set
((<%(A *^ (exp (NAT,a)))%> . s),NAT) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,1) is epsilon-transitive epsilon-connected ordinal set
1 *^ (exp (NAT,1)) is epsilon-transitive epsilon-connected ordinal set
<%(1 *^ (exp (NAT,1)))%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
a is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
a ^ A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom (a ^ A) is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ (dom A) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . b is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . b is epsilon-transitive epsilon-connected ordinal set
((a . b),NAT) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
a . s is epsilon-transitive epsilon-connected ordinal set
((a . s),NAT) is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . b is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . s is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ b is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . ((dom a) +^ b) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
((A . b),NAT) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
A . s is epsilon-transitive epsilon-connected ordinal set
((A . s),NAT) is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ b is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . ((dom a) +^ b) is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ s is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . ((dom a) +^ s) is epsilon-transitive epsilon-connected ordinal set
a is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() () () () set
len a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
dom a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
c3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
1 +^ c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
b is Relation-like Function-like T-Sequence-like set
s is Relation-like Function-like T-Sequence-like set
b ^ s is Relation-like Function-like T-Sequence-like set
dom b is epsilon-transitive epsilon-connected ordinal set
dom s is epsilon-transitive epsilon-connected ordinal set
c is Relation-like Function-like T-Sequence-like Ordinal-yielding set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
c ^ A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
B is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() () () () set
B . 0 is epsilon-transitive epsilon-connected ordinal set
c is non empty epsilon-transitive epsilon-connected ordinal () set
<%c%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
c9 is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() () () () set
<%c%> ^ c9 is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
len B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
dom B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() () () () set
a . 0 is epsilon-transitive epsilon-connected ordinal set
((a . 0),NAT) is epsilon-transitive epsilon-connected ordinal set
A is non empty epsilon-transitive epsilon-connected ordinal () set
(A,NAT) is epsilon-transitive epsilon-connected ordinal set
<%A%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
<%A%> ^ a is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
dom <%A%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative Element of K19(NAT)
<%A%> . 0 is epsilon-transitive epsilon-connected ordinal set
dom (<%A%> ^ a) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of K19(NAT)
dom a is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of K19(NAT)
1 +^ (dom a) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
b is epsilon-transitive epsilon-connected ordinal set
(<%A%> ^ a) . b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
1 +^ s is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
1 +^ s is epsilon-transitive epsilon-connected ordinal set
(<%A%> ^ a) . b is epsilon-transitive epsilon-connected ordinal set
a . s is epsilon-transitive epsilon-connected ordinal set
dom (<%A%> ^ a) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
b is epsilon-transitive epsilon-connected ordinal set
(<%A%> ^ a) . b is epsilon-transitive epsilon-connected ordinal set
(((<%A%> ^ a) . b),NAT) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
(<%A%> ^ a) . s is epsilon-transitive epsilon-connected ordinal set
(((<%A%> ^ a) . s),NAT) is epsilon-transitive epsilon-connected ordinal set
(1 +^ (dom a)) -^ 1 is epsilon-transitive epsilon-connected ordinal set
s -^ 1 is epsilon-transitive epsilon-connected ordinal set
b -^ 1 is epsilon-transitive epsilon-connected ordinal set
1 +^ (s -^ 1) is epsilon-transitive epsilon-connected ordinal set
1 +^ (b -^ 1) is epsilon-transitive epsilon-connected ordinal set
a . (b -^ 1) is epsilon-transitive epsilon-connected ordinal set
a . (s -^ 1) is epsilon-transitive epsilon-connected ordinal set
<%A%> . b is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
s -^ 1 is epsilon-transitive epsilon-connected ordinal set
(1 +^ (dom a)) -^ 1 is epsilon-transitive epsilon-connected ordinal set
1 +^ (s -^ 1) is epsilon-transitive epsilon-connected ordinal set
a . (s -^ 1) is epsilon-transitive epsilon-connected ordinal set
((a . (s -^ 1)),NAT) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A,NAT) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A,NAT)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c3 *^ (exp (NAT,(A,NAT))) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(c3 *^ (exp (NAT,(A,NAT)))) +^ b is epsilon-transitive epsilon-connected ordinal set
<%(c3 *^ (exp (NAT,(A,NAT))))%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
A is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() () () () set
(A) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() () () () set
(A) is epsilon-transitive epsilon-connected ordinal set
A . 0 is epsilon-transitive epsilon-connected ordinal set
dom A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of K19(NAT)
((A . 0),NAT) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((A . 0),NAT)) is epsilon-transitive epsilon-connected ordinal set
s is non empty epsilon-transitive epsilon-connected ordinal () set
(s,NAT) is epsilon-transitive epsilon-connected ordinal set
<%s%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
<%s%> ^ A is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() set
B is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() () () () set
(B) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like T-Sequence-like finite Ordinal-yielding V53() () () () set
(A) is epsilon-transitive epsilon-connected ordinal set
A is Relation-like NAT -defined Function-like non empty T-Sequence-like finite Ordinal-yielding V53() () () () set
(A) is epsilon-transitive epsilon-connected ordinal set