:: NEWTON semantic presentation

REAL is non empty V12() non finite V61() V62() V63() V67() set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V61() V62() V63() V64() V65() V66() V67() Element of K19(REAL)
K19(REAL) is V12() non finite set
COMPLEX is non empty V12() non finite V61() V67() set
RAT is non empty V12() non finite V61() V62() V63() V64() V67() set
INT is non empty V12() non finite V61() V62() V63() V64() V65() V67() set
K20(COMPLEX,COMPLEX) is V12() non finite complex-valued set
K19(K20(COMPLEX,COMPLEX)) is V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is V12() non finite complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V12() non finite set

K19(K20(REAL,REAL)) is V12() non finite set

K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set

K19(K20(RAT,RAT)) is V12() non finite set
K20(K20(RAT,RAT),RAT) is V5( RAT ) V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is V12() non finite set

K19(K20(INT,INT)) is V12() non finite set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is V12() non finite set

K19(K20(K20(NAT,NAT),NAT)) is V12() non finite set
omega is non empty V12() epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V61() V62() V63() V64() V65() V66() V67() set
K19(omega) is V12() non finite set
K19(NAT) is V12() non finite set
K232(NAT) is V39() set
{} is set

K258(REAL,(),K207()) is complex real ext-real Element of REAL
Seg 1 is non empty V12() finite 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty V12() finite V44() 1 -element V61() V62() V63() V64() V65() V66() set
Seg 2 is non empty finite 2 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is finite V44() V61() V62() V63() V64() V65() V66() set

id (Seg 1) is V1() V4( Seg 1) V5( RAT ) V5( INT ) V5( Seg 1) non empty total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg 1),(Seg 1)))

K19(K20((Seg 1),(Seg 1))) is finite V44() set

[1,1] is set
{1,1} is finite V44() V61() V62() V63() V64() V65() V66() set
{{1,1},{1}} is finite V44() set
{[1,1]} is non empty V12() finite 1 -element set

id (Seg 2) is V1() V4( Seg 2) V5( RAT ) V5( INT ) V5( Seg 2) non empty total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg 2),(Seg 2)))

K19(K20((Seg 2),(Seg 2))) is finite V44() set

[1,2] is set
{{1,2},{1}} is finite V44() set
{[1,2]} is non empty V12() finite 1 -element set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( not b1 <= 1 & not m <= b1 ) } is set
{1} \/ { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( not b1 <= 1 & not m <= b1 ) } is set
{m} is non empty V12() finite V44() 1 -element V61() V62() V63() V64() V65() V66() set
({1} \/ { b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( not b1 <= 1 & not m <= b1 ) } ) \/ {m} is set
k is set
n is set

k is set

K207() [;] (m,()) is set

{ b1 where b1 is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like Element of REAL * : len b1 = len k } is set

dom k is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)

K207() [;] (m,()) is set

dom (m * k) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)

m is complex set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
(Seg k) --> m is V1() V4( Seg k) V5({m}) Function-like V30( Seg k,{m}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg k),{m}))
{m} is non empty V12() finite 1 -element V61() set
K20((Seg k),{m}) is finite complex-valued set
K19(K20((Seg k),{m})) is finite V44() set

m is complex set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
(Seg k) --> m is V1() V4( Seg k) V5({m}) Function-like V30( Seg k,{m}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg k),{m}))
{m} is non empty V12() finite 1 -element V61() set
K20((Seg k),{m}) is finite complex-valued set
K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex set

(m,k) is set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

{m} is non empty V12() finite 1 -element V61() V62() V63() set

K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex real ext-real set

(m,k) is complex real ext-real set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

{m} is non empty V12() finite 1 -element V61() V62() V63() set

K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex real ext-real set
m is complex set

(m,k) is set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
(Seg k) --> m is V1() V4( Seg k) V5({m}) Function-like V30( Seg k,{m}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg k),{m}))
{m} is non empty V12() finite 1 -element V61() set
K20((Seg k),{m}) is finite complex-valued set
K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex set
m is complex set
(m,0) is complex set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

{m} is non empty V12() finite 1 -element V61() set
K20((),{m}) is finite complex-valued set
K19(K20((),{m})) is finite V44() set

m is complex set
(m,1) is complex set

(Seg 1) --> m is V1() V4( Seg 1) V5({m}) Function-like V30( Seg 1,{m}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg 1),{m}))
{m} is non empty V12() finite 1 -element V61() set
K20((Seg 1),{m}) is finite complex-valued set
K19(K20((Seg 1),{m})) is finite V44() set
Product (1 |-> m) is complex set

[1,m] is set
{1,m} is finite V61() set
{{1,m},{1}} is finite V44() set
{[1,m]} is non empty V12() finite 1 -element set

k is complex set
(k,(m + 1)) is complex set

Seg (m + 1) is non empty finite m + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m + 1 ) } is set
(Seg (m + 1)) --> k is V1() V4( Seg (m + 1)) V5({k}) Function-like V30( Seg (m + 1),{k}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg (m + 1)),{k}))
{k} is non empty V12() finite 1 -element V61() set
K20((Seg (m + 1)),{k}) is finite complex-valued set
K19(K20((Seg (m + 1)),{k})) is finite V44() set
Product ((m + 1) |-> k) is complex set
(k,m) is complex set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(Seg m) --> k is V1() V4( Seg m) V5({k}) Function-like V30( Seg m,{k}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{k}))
K20((Seg m),{k}) is finite complex-valued set
K19(K20((Seg m),{k})) is finite V44() set
Product (m |-> k) is complex set
(k,m) * k is complex set

[1,k] is set
{1,k} is finite V61() set
{{1,k},{1}} is finite V44() set
{[1,k]} is non empty V12() finite 1 -element set

Product ((m |-> k) ^ <*k*>) is complex set

(m,k) is complex real ext-real set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

{m} is non empty V12() finite V44() 1 -element V61() V62() V63() V64() V65() V66() set

K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex real ext-real set

(m,n) is complex real ext-real set

Seg n is finite n -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

K19(K20((Seg n),{m})) is finite V44() set
Product (n |-> m) is complex real ext-real set

(m,(n + 1)) is complex real ext-real set

Seg (n + 1) is non empty finite n + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= n + 1 ) } is set
(Seg (n + 1)) --> m is V1() V4( Seg (n + 1)) V5( INT ) V5({m}) Function-like V30( Seg (n + 1),{m}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg (n + 1)),{m}))

K19(K20((Seg (n + 1)),{m})) is finite V44() set
Product ((n + 1) |-> m) is complex real ext-real set

(m,0) is complex real ext-real set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

K19(K20((),{m})) is finite V44() set

k is complex set
(k,m) is complex set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(Seg m) --> k is V1() V4( Seg m) V5({k}) Function-like V30( Seg m,{k}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{k}))
{k} is non empty V12() finite 1 -element V61() set
K20((Seg m),{k}) is finite complex-valued set
K19(K20((Seg m),{k})) is finite V44() set
Product (m |-> k) is complex set
n is complex set
k * n is complex set
((k * n),m) is complex set

(Seg m) --> (k * n) is V1() V4( Seg m) V5({(k * n)}) Function-like V30( Seg m,{(k * n)}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{(k * n)}))
{(k * n)} is non empty V12() finite 1 -element V61() set
K20((Seg m),{(k * n)}) is finite complex-valued set
K19(K20((Seg m),{(k * n)})) is finite V44() set
Product (m |-> (k * n)) is complex set
(n,m) is complex set

(Seg m) --> n is V1() V4( Seg m) V5({n}) Function-like V30( Seg m,{n}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{n}))
{n} is non empty V12() finite 1 -element V61() set
K20((Seg m),{n}) is finite complex-valued set
K19(K20((Seg m),{n})) is finite V44() set
Product (m |-> n) is complex set
(k,m) * (n,m) is complex set

(t,m) is complex set

(Seg m) --> t is V1() V4( Seg m) V5({t}) Function-like V30( Seg m,{t}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{t}))
{t} is non empty V12() finite 1 -element V61() set
K20((Seg m),{t}) is finite complex-valued set
K19(K20((Seg m),{t})) is finite V44() set
Product (m |-> t) is complex set

(t,m) is complex set

(Seg m) --> t is V1() V4( Seg m) V5({t}) Function-like V30( Seg m,{t}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{t}))
{t} is non empty V12() finite 1 -element V61() set
K20((Seg m),{t}) is finite complex-valued set
K19(K20((Seg m),{t})) is finite V44() set
Product (m |-> t) is complex set
(t,m) * (t,m) is complex set
t * t is complex set

(Seg m) --> (t * t) is V1() V4( Seg m) V5({(t * t)}) Function-like V30( Seg m,{(t * t)}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{(t * t)}))
{(t * t)} is non empty V12() finite 1 -element V61() set
K20((Seg m),{(t * t)}) is finite complex-valued set
K19(K20((Seg m),{(t * t)})) is finite V44() set
Product (m |-> (t * t)) is complex set

n is complex set
(n,(m + k)) is complex set

Seg (m + k) is finite m + k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m + k ) } is set
(Seg (m + k)) --> n is V1() V4( Seg (m + k)) V5({n}) Function-like V30( Seg (m + k),{n}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg (m + k)),{n}))
{n} is non empty V12() finite 1 -element V61() set
K20((Seg (m + k)),{n}) is finite complex-valued set
K19(K20((Seg (m + k)),{n})) is finite V44() set
Product ((m + k) |-> n) is complex set
(n,m) is complex set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(Seg m) --> n is V1() V4( Seg m) V5({n}) Function-like V30( Seg m,{n}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{n}))
K20((Seg m),{n}) is finite complex-valued set
K19(K20((Seg m),{n})) is finite V44() set
Product (m |-> n) is complex set
(n,k) is complex set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
(Seg k) --> n is V1() V4( Seg k) V5({n}) Function-like V30( Seg k,{n}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg k),{n}))
K20((Seg k),{n}) is finite complex-valued set
K19(K20((Seg k),{n})) is finite V44() set
Product (k |-> n) is complex set
(n,m) * (n,k) is complex set

(t,m) is complex set

(Seg m) --> t is V1() V4( Seg m) V5({t}) Function-like V30( Seg m,{t}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{t}))
{t} is non empty V12() finite 1 -element V61() set
K20((Seg m),{t}) is finite complex-valued set
K19(K20((Seg m),{t})) is finite V44() set
Product (m |-> t) is complex set
(t,k) is complex set

(Seg k) --> t is V1() V4( Seg k) V5({t}) Function-like V30( Seg k,{t}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg k),{t}))
K20((Seg k),{t}) is finite complex-valued set
K19(K20((Seg k),{t})) is finite V44() set
Product (k |-> t) is complex set
(t,m) * (t,k) is complex set

{ b1 where b1 is V1() V4( NAT ) V5( COMPLEX ) Function-like finite FinSequence-like FinSubsequence-like Element of COMPLEX * : len b1 = m + k } is set
(Seg (m + k)) --> t is V1() V4( Seg (m + k)) V5({t}) Function-like V30( Seg (m + k),{t}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg (m + k)),{t}))
K20((Seg (m + k)),{t}) is finite complex-valued set
K19(K20((Seg (m + k)),{t})) is finite V44() set
Product ((m + k) |-> t) is complex Element of COMPLEX

K258(COMPLEX,((m + k) |-> t),K201()) is complex Element of COMPLEX

n is complex set
(n,m) is complex set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(Seg m) --> n is V1() V4( Seg m) V5({n}) Function-like V30( Seg m,{n}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{n}))
{n} is non empty V12() finite 1 -element V61() set
K20((Seg m),{n}) is finite complex-valued set
K19(K20((Seg m),{n})) is finite V44() set
Product (m |-> n) is complex set
((n,m),k) is complex set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
(Seg k) --> (n,m) is V1() V4( Seg k) V5({(n,m)}) Function-like V30( Seg k,{(n,m)}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg k),{(n,m)}))
{(n,m)} is non empty V12() finite 1 -element V61() set
K20((Seg k),{(n,m)}) is finite complex-valued set
K19(K20((Seg k),{(n,m)})) is finite V44() set
Product (k |-> (n,m)) is complex set
(n,(m * k)) is complex set

Seg (m * k) is finite m * k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m * k ) } is set
(Seg (m * k)) --> n is V1() V4( Seg (m * k)) V5({n}) Function-like V30( Seg (m * k),{n}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg (m * k)),{n}))
K20((Seg (m * k)),{n}) is finite complex-valued set
K19(K20((Seg (m * k)),{n})) is finite V44() set
Product ((m * k) |-> n) is complex set

(t,(m * k)) is complex set

(Seg (m * k)) --> t is V1() V4( Seg (m * k)) V5({t}) Function-like V30( Seg (m * k),{t}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg (m * k)),{t}))
{t} is non empty V12() finite 1 -element V61() set
K20((Seg (m * k)),{t}) is finite complex-valued set
K19(K20((Seg (m * k)),{t})) is finite V44() set
Product ((m * k) |-> t) is complex set
(t,m) is complex set

(Seg m) --> t is V1() V4( Seg m) V5({t}) Function-like V30( Seg m,{t}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg m),{t}))
K20((Seg m),{t}) is finite complex-valued set
K19(K20((Seg m),{t})) is finite V44() set
Product (m |-> t) is complex set

(Seg k) --> (t,m) is V1() V4( Seg k) V5({(t,m)}) Function-like V30( Seg k,{(t,m)}) finite FinSequence-like FinSubsequence-like complex-valued Element of K19(K20((Seg k),{(t,m)}))
{(t,m)} is non empty V12() finite 1 -element V61() set
K20((Seg k),{(t,m)}) is finite complex-valued set
K19(K20((Seg k),{(t,m)})) is finite V44() set
Product (k |-> (t,m)) is complex set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set

K19(K20((Seg m),{1})) is finite V44() set
Product (m |-> 1) is complex real ext-real set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

K19(K20((Seg k),{1})) is finite V44() set
Product (k |-> 1) is complex real ext-real set

Seg (k + 1) is non empty finite k + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k + 1 ) } is set
(Seg (k + 1)) --> 1 is V1() V4( Seg (k + 1)) V5( RAT ) V5( INT ) V5({1}) Function-like V30( Seg (k + 1),{1}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg (k + 1)),{1}))

K19(K20((Seg (k + 1)),{1})) is finite V44() set
Product ((k + 1) |-> 1) is complex real ext-real set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

K19(K20((),{1})) is finite V44() set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set

is non empty V12() finite V44() 1 -element V61() V62() V63() V64() V65() V66() set

K19(K20((Seg m),)) is finite V44() set

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set

K19(K20((Seg k),)) is finite V44() set

Seg (k + 1) is non empty finite k + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k + 1 ) } is set
(Seg (k + 1)) --> 0 is V1() V4( Seg (k + 1)) V5( RAT ) V5( INT ) V5() Function-like V30( Seg (k + 1),) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg (k + 1)),))

K19(K20((Seg (k + 1)),)) is finite V44() set
Product ((k + 1) |-> 0) is complex real ext-real set

K19(K20((Seg 1),)) is finite V44() set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is V1() V4( Seg m) V5( RAT ) V5( INT ) V5( Seg m) total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),(Seg m)))

K19(K20((Seg m),(Seg m))) is finite V44() set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is V1() V4( Seg m) V5( RAT ) V5( INT ) V5( Seg m) total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),(Seg m)))

K19(K20((Seg m),(Seg m))) is finite V44() set

(m) is complex real ext-real Element of REAL

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is V1() V4( Seg m) V5( RAT ) V5( INT ) V5( Seg m) total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),(Seg m)))

K19(K20((Seg m),(Seg m))) is finite V44() set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

K19(K20((),())) is finite V44() set

(1) is complex real ext-real Element of REAL

(2) is complex real ext-real Element of REAL

((m + 1)) is complex real ext-real Element of REAL

Seg (m + 1) is non empty finite m + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m + 1 ) } is set
id (Seg (m + 1)) is V1() V4( Seg (m + 1)) V5( RAT ) V5( INT ) V5( Seg (m + 1)) non empty total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg (m + 1)),(Seg (m + 1))))
K20((Seg (m + 1)),(Seg (m + 1))) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg (m + 1)),(Seg (m + 1)))) is finite V44() set
Product (idseq (m + 1)) is complex real ext-real set
(m) is complex real ext-real Element of REAL

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is V1() V4( Seg m) V5( RAT ) V5( INT ) V5( Seg m) total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),(Seg m)))

K19(K20((Seg m),(Seg m))) is finite V44() set

(m) * (m + 1) is complex real ext-real Element of REAL

[1,(m + 1)] is set
{1,(m + 1)} is finite V44() V61() V62() V63() V64() V65() V66() set
{{1,(m + 1)},{1}} is finite V44() set
{[1,(m + 1)]} is non empty V12() finite 1 -element set

(m) is complex real ext-real Element of REAL

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is V1() V4( Seg m) V5( RAT ) V5( INT ) V5( Seg m) total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),(Seg m)))

K19(K20((Seg m),(Seg m))) is finite V44() set

(k) is complex real ext-real Element of REAL

Seg k is finite k -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k ) } is set
id (Seg k) is V1() V4( Seg k) V5( RAT ) V5( INT ) V5( Seg k) total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg k),(Seg k)))

K19(K20((Seg k),(Seg k))) is finite V44() set

((k + 1)) is complex real ext-real Element of REAL

Seg (k + 1) is non empty finite k + 1 -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= k + 1 ) } is set
id (Seg (k + 1)) is V1() V4( Seg (k + 1)) V5( RAT ) V5( INT ) V5( Seg (k + 1)) non empty total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg (k + 1)),(Seg (k + 1))))
K20((Seg (k + 1)),(Seg (k + 1))) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg (k + 1)),(Seg (k + 1)))) is finite V44() set
Product (idseq (k + 1)) is complex real ext-real set

(m) is complex real ext-real Element of REAL

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is V1() V4( Seg m) V5( RAT ) V5( INT ) V5( Seg m) total finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),(Seg m)))

K19(K20((Seg m),(Seg m))) is finite V44() set

Seg m is finite m -element V61() V62() V63() V64() V65() V66() Element of K19(NAT)
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set