:: NAT_1 semantic presentation

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

F

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

F

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

F

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

F

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

F

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

F

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

F

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

F

x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal Element of NAT

F

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

F

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

F

F

F

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

{ b

{ b

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

{ b

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

{ b

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)

F

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

F

succ x1 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal set

F

K7(NAT,F

K6(K7(NAT,F

F

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

F

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 F

x1 . 0 is Element of F

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 F

x1 . x is set

F

F

dom F

F

F

F

dom F

F

n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

F

F

(n,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT

F

F

n is set

F

F

F

K7(NAT,F

K6(K7(NAT,F

F

F

F

F

F

dom F

dom F

n is set

F

F

n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

F

F

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

F

F

(x,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT

F

F

F

dom F

F

F

F

dom F

F

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

F

F

F

x is set

n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

x1 is set

F

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

F

F

F

F

K7(NAT,F

K6(K7(NAT,F

F

F

F

F

F

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

F

F

F

x is Element of F

n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

x1 is Element of F

F

x is Element of F

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

F

F

F

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

F

x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

F

(x1,1) is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real finite cardinal Element of NAT

F

F

n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

F

n is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

F

x1 is epsilon-transitive epsilon-connected ordinal natural complex ext-real non negative real finite cardinal set

F

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

{ b

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

{ H

{ H

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

F

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

F

(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

F

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