:: NAT_1 semantic presentation

REAL is non empty non finite set

K6(REAL) is non empty non finite set

K6(omega) is non empty non finite set
{} is set

n is Element of K6(REAL)

x1 + 1 is complex ext-real real set

x is Element of K6(REAL)

(n + x) + 1 is complex ext-real real set

n + (x + 1) is complex ext-real real set

nn + 1 is complex ext-real real set
(n + nn) + 1 is complex ext-real real set

x1 is Element of K6(REAL)

n * (x,1) 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 + (- x1) is complex ext-real real set
(x1,1) + (- x1) is complex ext-real real set

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

x1 - 1 is complex ext-real real set

n is set
K6(NAT) is non empty non finite set
the Element of n is Element of n

{ 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
{ } is set
x1 is set

x1 is set

x1 is set
x is set
n is finite set
x1 is finite 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

{ 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 /\ x1 is set
Segm n is Element of K6(omega)
Segm x1 is Element of K6(omega)
F1() is set

n . {} is set
n . 0 is set

n . (x1,1) is set
n . x1 is set
F2(x1,(n . x1)) 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
F2() is Element of F1()

dom n is set
n . 0 is set
x1 is set
n . x1 is set

n . x is set
n . x is set
F3(x,(n . x)) is Element of F1()

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()

x1 . (x,1) is Element of F1()
x1 . x is set
F3(x,(x1 . x)) is Element of F1()

dom F2() is set
F2() . 0 is set
F1() is set

dom F3() is set
F3() . 0 is set

F2() . n is set
F3() . n is set

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

F3() . n is set
F4() . n is set

F3() . x is Element of F1()
F4() . x is Element of F1()

F3() . (x,1) is Element of F1()
F4() . (x,1) is Element of F1()

dom F3() is set
F3() . 0 is set
F1() is set

dom F4() is set
F4() . 0 is set

F4() . (n,1) is set
F4() . n is set
F2(n,(F4() . n)) is set
x is set

x1 is set
F2(n,x1) is set
x is set

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()

F5() . (n,1) is Element of F1()
F5() . n is set
F3(n,(F5() . n)) is Element of F1()
x is Element of F1()

x1 is Element of F1()
F3(n,x1) is Element of F1()
x is Element of F1()

F4() . (n,1) is Element of F1()
F4() . n is set
F3(n,(F4() . n)) is Element of F1()

min (n,x1) is complex ext-real real set
max (n,x1) is complex ext-real real 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))

x1 . x is set

x1 . x is Element of n

x is set

n . (x,x1) is set
x is set

x . x is set

n . (x + x1) is set

n . (x,x1) is set

x is set
x . x is set

n . (nn,x1) is set
x . x is set

rng n is 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

n . (x,x1) is set
n is non empty 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))

(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))

(n,(n,x1,0),x) is Element of n

(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))

(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))

(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,(n,(n,x1,x),x),x) is Element of n

(n,(n,x1,x),(x,x)) is Element of n

(n,x1,((x,x),x)) is Element of n

(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))

(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))
(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))

(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

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

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

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

(n,(n,(x1 * x),x),x) is Element of n

(n,(x1 * x),(x,x)) is Element of n

(n,x1,(NAT,x,(x,x))) is Element of n

(n,x1,(NAT,(NAT,x,x),x)) is Element of n
(n,(x1 * (NAT,x,x)),x) is Element of n

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

{ } is set

{ 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

rng n is set
x1 is set
dom n is set
x is set
n . x is set

x1 is non empty Element of K6(NAT)

dom n is set
x is set
n . x is 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,x1) is non empty Relation-like NAT -defined Function-like total set
rng (n,x1) is set
rng n is set

n is finite set

choose n is Element of n
x is set
{()} is non empty V2() 1 -element set
x is set