REAL is non empty non finite set
NAT is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is non empty non finite set
omega is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
K6(omega) is non empty non finite set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real finite cardinal {} -element set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real finite cardinal {} -element set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is Element of K6(REAL)
x1 is complex ext-real real set
x1 + 1 is complex ext-real real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x1 is complex ext-real real set
x is Element of K6(REAL)
x is complex ext-real real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x is complex ext-real real set
(n + x) + 1 is complex ext-real real set
x + 1 is complex ext-real real set
n + (x + 1) is complex ext-real real set
nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n + nn is complex ext-real real set
nn + 1 is complex ext-real real set
(n + nn) + 1 is complex ext-real real set
x + 1 is complex ext-real real set
n + 0 is complex ext-real real set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x is complex ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is Element of K6(REAL)
x is complex ext-real real Element of REAL
x + 1 is complex ext-real real set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(x,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(n,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x1 is complex ext-real real set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x is complex ext-real real set
(x,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n * (x,1) is complex ext-real real set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x + n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * 0 is complex ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n * x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(x1,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 + n is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
F1() is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
F2((x1,1),x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
F2((x1,1),nn) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(u,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
w is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
F2((x1,1),w) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
F2(0,x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
F2(0,x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
((n + x),1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(n,(x,1)) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(n,0) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + 0 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(0,n) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
F1() is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
- x is complex ext-real real set
(- x) + x is complex ext-real real set
((- x) + x) + 1 is complex ext-real real set
(- x) + (x,1) is complex ext-real real set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n,0) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
- x1 is complex ext-real real set
x1 + (- x1) is complex ext-real real set
(x1,1) + (- x1) is complex ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(0,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x * x) + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
((x * x) + x) + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
((((x * x) + x) + x),1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(0,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 + n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n * x) + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
nn is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(n * x) + nn is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
((n * x),nn) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(n * x) + nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n,x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
((n,x),nn) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n * x) + nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n * u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
w is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n * u) + w is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(n,0) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
((n,0),0) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * x) + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * x) + nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x + u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 * (x + u) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * (x + u)) + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 * u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * u) + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * x) + ((x1 * u) + x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
w is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(w,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x1 * w is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * w) + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 + ((x1 * w) + x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x + u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 * (x + u) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * (x + u)) + nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 * u is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * u) + nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * x) + ((x1 * u) + nn) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
w is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(w,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x1 * w is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1 * w) + nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 + ((x1 * w) + nn) is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 - 1 is complex ext-real real set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
((n,1),x) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 - n is complex ext-real real set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
((n,1),x) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
(1,x) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
(1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x * n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x * x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x,1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
((x * x),(x,1)) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
F1() is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
F1() + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
((n,x1),1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F1() + (x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1() + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1() + 0 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1() is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(0,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(2,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(3,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
5 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(4,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
6 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(5,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
7 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(6,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
8 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(7,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
9 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(8,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
10 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(9,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
11 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(10,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
12 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(11,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
13 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(12,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal set
n is set
K6(NAT) is non empty non finite set
the Element of n is Element of n
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of omega
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT : not (n,1) <= b1 } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT : not n <= b1 } is set
x1 is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
((x,1),x) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(x,nn) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
succ x is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of omega
succ (x,nn) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of omega
((x,nn),1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
succ x is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of omega
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
card n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
card x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
card x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
card x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
card n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
card x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
card n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
nextcard (card n) is epsilon-transitive epsilon-connected ordinal cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
card (n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of omega
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
card x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
card (card x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
card (x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of omega
x is epsilon-transitive epsilon-connected ordinal cardinal set
succ x1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of omega
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 is set
x is set
n is finite set
x1 is finite set
card n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
card x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT : not x1 <= b1 } is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT : not (x1,1) <= b1 } is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n /\ x1 is set
Segm n is Element of K6(omega)
Segm x1 is Element of K6(omega)
F1() is set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is set
n . 0 is set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n . (x1,1) is set
n . x1 is set
F2(x1,(n . x1)) is set
succ x1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal set
F1() is non empty set
K7(NAT,F1()) is non empty non finite set
K6(K7(NAT,F1())) is non empty non finite set
F2() is Element of F1()
n is Relation-like Function-like set
dom n is set
n . 0 is set
x1 is set
n . x1 is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n . x is set
n . x is set
F3(x,(n . x)) is Element of F1()
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is non empty Relation-like NAT -defined F1() -valued Function-like total V38( NAT ,F1()) Element of K6(K7(NAT,F1()))
x1 . 0 is Element of F1()
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 . (x,1) is Element of F1()
x1 . x is set
F3(x,(x1 . x)) is Element of F1()
F2() is Relation-like Function-like set
dom F2() is set
F2() . 0 is set
F1() is set
F3() is Relation-like Function-like set
dom F3() is set
F3() . 0 is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F2() . n is set
F3() . n is set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F2() . (n,1) is set
F3() . (n,1) is set
n is set
F2() . n is set
F3() . n is set
F1() is non empty set
K7(NAT,F1()) is non empty non finite set
K6(K7(NAT,F1())) is non empty non finite set
F3() is non empty Relation-like NAT -defined F1() -valued Function-like total V38( NAT ,F1()) Element of K6(K7(NAT,F1()))
F3() . 0 is Element of F1()
F2() is Element of F1()
F4() is non empty Relation-like NAT -defined F1() -valued Function-like total V38( NAT ,F1()) Element of K6(K7(NAT,F1()))
F4() . 0 is Element of F1()
dom F3() is set
dom F4() is set
n is set
F3() . n is set
F4() . n is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F3() . n is set
F4() . n is set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
F3() . x is Element of F1()
F4() . x is Element of F1()
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F3() . (x,1) is Element of F1()
F4() . (x,1) is Element of F1()
F3() is Relation-like Function-like set
dom F3() is set
F3() . 0 is set
F1() is set
F4() is Relation-like Function-like set
dom F4() is set
F4() . 0 is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F4() . (n,1) is set
F4() . n is set
F2(n,(F4() . n)) is set
x is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is set
F2(n,x1) is set
x is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F3() . (n,1) is set
F3() . n is set
F2(n,(F3() . n)) is set
F1() is non empty set
K7(NAT,F1()) is non empty non finite set
K6(K7(NAT,F1())) is non empty non finite set
F4() is non empty Relation-like NAT -defined F1() -valued Function-like total V38( NAT ,F1()) Element of K6(K7(NAT,F1()))
F4() . 0 is Element of F1()
F2() is Element of F1()
F5() is non empty Relation-like NAT -defined F1() -valued Function-like total V38( NAT ,F1()) Element of K6(K7(NAT,F1()))
F5() . 0 is Element of F1()
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F5() . (n,1) is Element of F1()
F5() . n is set
F3(n,(F5() . n)) is Element of F1()
x is Element of F1()
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is Element of F1()
F3(n,x1) is Element of F1()
x is Element of F1()
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F4() . (n,1) is Element of F1()
F4() . n is set
F3(n,(F4() . n)) is Element of F1()
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
min (n,x1) is complex ext-real real set
max (n,x1) is complex ext-real real set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
min (n,x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
max (n,x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1(x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1(x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
F1((x1,1)) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1(0) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1(n) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1(n) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
F1(x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is set
K7(NAT,n) is set
K6(K7(NAT,n)) is non empty set
x1 is Relation-like NAT -defined n -valued Function-like V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 . x is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x1 . x is Element of n
n is non empty Relation-like NAT -defined Function-like total set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(x,x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n . (x,x1) is set
x is set
x is non empty Relation-like NAT -defined Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x . x is set
x + x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n . (x + x1) is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(x,x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n . (x,x1) is set
x is non empty Relation-like NAT -defined Function-like total set
x is non empty Relation-like NAT -defined Function-like total set
x is set
x . x is set
nn is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(nn,x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n . (nn,x1) is set
x . x is set
n is non empty Relation-like NAT -defined Function-like total set
rng n is set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,x1) is non empty Relation-like NAT -defined Function-like total set
rng (n,x1) is set
x is set
dom (n,x1) is set
x is set
(n,x1) . x is set
dom n is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(x,x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n . (x,x1) is set
n is non empty set
x1 is non empty Relation-like NAT -defined n -valued Function-like total set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x1,x) is non empty Relation-like NAT -defined Function-like total set
rng (x1,x) is set
rng x1 is set
n is non empty set
K7(NAT,n) is non empty non finite set
K6(K7(NAT,n)) is non empty non finite set
x1 is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(x1,x) is non empty Relation-like NAT -defined n -valued Function-like total set
rng (x1,x) is set
dom (x1,x) is set
n is non empty set
K7(NAT,n) is non empty non finite set
K6(K7(NAT,n)) is non empty non finite set
x1 is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
(n,x1,0) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,(n,x1,0),x) is Element of n
(x,0) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,x1,(x,0)) is Element of n
(n,x1,x) is Element of n
n is non empty set
K7(NAT,n) is non empty non finite set
K6(K7(NAT,n)) is non empty non finite set
x1 is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,x1,x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,(n,x1,x),x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,x1,(x + x)) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,(n,(n,x1,x),x),x) is Element of n
(x,x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,(n,x1,x),(x,x)) is Element of n
((x,x),x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,x1,((x,x),x)) is Element of n
(x,(x + x)) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,x1,(x,(x + x))) is Element of n
(n,(n,x1,(x + x)),x) is Element of n
n is non empty set
K7(NAT,n) is non empty non finite set
K6(K7(NAT,n)) is non empty non finite set
x1 is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,x1,x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,(n,x1,x),x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
(n,x1,x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
(n,(n,x1,x),x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x + x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,x1,(x + x)) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
K7(NAT,NAT) is non empty non finite set
K6(K7(NAT,NAT)) is non empty non finite set
x1 is non empty set
K7(NAT,x1) is non empty non finite set
K6(K7(NAT,x1)) is non empty non finite set
n is non empty Relation-like NAT -defined NAT -valued Function-like total V38( NAT , NAT ) Element of K6(K7(NAT,NAT))
x is non empty Relation-like NAT -defined x1 -valued Function-like total V38( NAT ,x1) Element of K6(K7(NAT,x1))
x * n is non empty Relation-like NAT -defined x1 -valued Function-like total V38( NAT ,x1) Element of K6(K7(NAT,x1))
x1 is non empty set
K7(NAT,x1) is non empty non finite set
K6(K7(NAT,x1)) is non empty non finite set
n is non empty Relation-like NAT -defined NAT -valued Function-like total V38( NAT , NAT ) Element of K6(K7(NAT,NAT))
x is non empty Relation-like NAT -defined x1 -valued Function-like total V38( NAT ,x1) Element of K6(K7(NAT,x1))
x * n is non empty Relation-like NAT -defined x1 -valued Function-like total V38( NAT ,x1) Element of K6(K7(NAT,x1))
n is non empty set
K7(NAT,n) is non empty non finite set
K6(K7(NAT,n)) is non empty non finite set
x1 is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x is non empty Relation-like NAT -defined NAT -valued Function-like total V38( NAT , NAT ) Element of K6(K7(NAT,NAT))
x1 * x is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
(n,(x1 * x),x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
(NAT,x,x) is non empty Relation-like NAT -defined NAT -valued Function-like total V38( NAT , NAT ) Element of K6(K7(NAT,NAT))
x1 * (NAT,x,x) is non empty Relation-like NAT -defined n -valued Function-like total V38( NAT ,n) Element of K6(K7(NAT,n))
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,(n,(x1 * x),x),x) is Element of n
(x,x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,(x1 * x),(x,x)) is Element of n
(NAT,x,(x,x)) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,x1,(NAT,x,(x,x))) is Element of n
(NAT,(NAT,x,x),x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(n,x1,(NAT,(NAT,x,x),x)) is Element of n
(n,(x1 * (NAT,x,x)),x) is Element of n
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is non empty set
K7(NAT,x1) is non empty non finite set
K6(K7(NAT,x1)) is non empty non finite set
x is non empty Relation-like NAT -defined x1 -valued Function-like total V38( NAT ,x1) Element of K6(K7(NAT,x1))
(x1,x,n) is Element of x1
rng x is set
dom x is set
n is set
x1 is non empty set
K7(NAT,x1) is non empty non finite set
K6(K7(NAT,x1)) is non empty non finite set
x is non empty Relation-like NAT -defined x1 -valued Function-like total V38( NAT ,x1) Element of K6(K7(NAT,x1))
rng x is set
x is set
dom x is set
x is set
x . x is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(0,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal set
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT : b1 <= n } is set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT : S2[b1] } is set
{ H1(b1) where b1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT : S1[b1] } is set
n is non empty Relation-like NAT -defined NAT -valued Function-like total V38( NAT , NAT ) Element of K6(K7(NAT,NAT))
(NAT,n,0) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
rng n is set
x1 is set
dom n is set
x is set
n . x is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
F1(x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
x1 is non empty Element of K6(NAT)
(x1) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
dom n is set
x is set
n . x is set
x is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(NAT,n,x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
F1(x) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(NAT,n,(x,1)) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
F1((x,1)) is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal set
x1 is set
n --> x1 is Relation-like n -defined {x1} -valued Function-like total V38(n,{x1}) Element of K6(K7(n,{x1}))
{x1} is non empty V2() 1 -element set
K7(n,{x1}) is set
K6(K7(n,{x1})) is non empty set
dom (n --> x1) is set
n is non empty Relation-like NAT -defined Function-like total set
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,x1) is non empty Relation-like NAT -defined Function-like total set
rng (n,x1) is set
rng n is set
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,2) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
((n,1),1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,3) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(n,2) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
((n,2),1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(n,4) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(n,2) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
(n,3) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
((n,3),1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is finite set
card n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of omega
choose n is Element of n
x is set
{(choose n)} is non empty V2() 1 -element set
x is set
14 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set
(13,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT