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
K20(REAL,REAL) is V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is V12() non finite set
K20(K20(REAL,REAL),REAL) is V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is V12() non finite set
K20(RAT,RAT) is V5( RAT ) V12() non finite complex-valued ext-real-valued real-valued 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
K20(INT,INT) is V5( RAT ) V5( INT ) V12() non finite complex-valued ext-real-valued real-valued 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
K20(NAT,NAT) is V5( RAT ) V5( INT ) V12() non finite complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) V12() non finite complex-valued ext-real-valued real-valued natural-valued 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
the functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite V44() cardinal {} -element FinSequence-membered V61() V62() V63() V64() V65() V66() V67() set is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite V44() cardinal {} -element FinSequence-membered V61() V62() V63() V64() V65() V66() V67() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
0 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
<*> REAL is V1() V4( NAT ) V5( REAL ) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() FinSequence of REAL
Product (<*> REAL) is complex real ext-real Element of REAL
K207() is V1() V4(K20(REAL,REAL)) V5( REAL ) Function-like V30(K20(REAL,REAL), REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))
K258(REAL,(<*> 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
idseq 1 is V1() V4( NAT ) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like 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)))
K20((Seg 1),(Seg 1)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg 1),(Seg 1))) is finite V44() set
<*1*> is V1() V4( NAT ) V5( NAT ) Function-like one-to-one non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V55() decreasing non-decreasing non-increasing FinSequence of NAT
[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
idseq 2 is V1() V4( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like 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)))
K20((Seg 2),(Seg 2)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg 2),(Seg 2))) is finite V44() set
<*1,2*> is V1() V4( NAT ) Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
<*1*> is V1() V4( NAT ) Function-like one-to-one non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V55() decreasing non-decreasing non-increasing set
<*2*> is V1() V4( NAT ) Function-like one-to-one non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V55() decreasing non-decreasing non-increasing set
[1,2] is set
{{1,2},{1}} is finite V44() set
{[1,2]} is non empty V12() finite 1 -element set
<*1*> ^ <*2*> is V1() V4( NAT ) Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
card {} is epsilon-transitive epsilon-connected ordinal cardinal set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal 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
t 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
k is set
n 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
m is complex real ext-real set
k is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
m * k is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K337(m) is V1() V4( REAL ) V5( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
id REAL is V1() V4( REAL ) V5( REAL ) non empty total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K207() [;] (m,(id REAL)) is set
K337(m) * k is V1() finite FinSequence-like complex-valued ext-real-valued real-valued set
len (m * k) 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
len k 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
(len k) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
{ 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
n is V1() V4( NAT ) V5( REAL ) Function-like finite len k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len k) -tuples_on REAL
m * n is V1() V4( NAT ) V5( REAL ) Function-like finite len k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (len k) -tuples_on REAL
K337(m) * n is V1() finite FinSequence-like complex-valued ext-real-valued real-valued set
len (m * n) 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
len n 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
k is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom k is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
m is complex real ext-real set
m * k is V1() V4( NAT ) V5( REAL ) Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K337(m) is V1() V4( REAL ) V5( REAL ) Function-like V30( REAL , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
id REAL is V1() V4( REAL ) V5( REAL ) non empty total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K207() [;] (m,(id REAL)) is set
K337(m) * k is V1() finite FinSequence-like complex-valued ext-real-valued real-valued set
dom (m * k) is finite V61() V62() V63() V64() V65() V66() Element of K19(NAT)
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
m is complex set
k |-> m is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like 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
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
m is complex set
k |-> m is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued 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 real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m,k) is set
k |-> m is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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 ext-real-valued real-valued Element of K19(K20((Seg k),{m}))
{m} is non empty V12() finite 1 -element V61() V62() V63() set
K20((Seg k),{m}) is finite complex-valued ext-real-valued real-valued set
K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex real ext-real set
m is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m,k) is complex real ext-real set
k |-> m is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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 ext-real-valued real-valued Element of K19(K20((Seg k),{m}))
{m} is non empty V12() finite 1 -element V61() V62() V63() set
K20((Seg k),{m}) is finite complex-valued ext-real-valued real-valued set
K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex real ext-real set
m is complex set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m,k) is set
k |-> m is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued 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
0 |-> m is V1() V4( NAT ) V5( RAT ) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite finite-yielding V44() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() set
Seg 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite V44() cardinal 0 -element FinSequence-membered V61() V62() V63() V64() V65() V66() V67() 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 <= 0 ) } is set
(Seg 0) --> m is V1() V4( Seg 0) V5({m}) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V30( Seg 0,{m}) integer finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() Element of K19(K20((Seg 0),{m}))
{m} is non empty V12() finite 1 -element V61() set
K20((Seg 0),{m}) is finite complex-valued set
K19(K20((Seg 0),{m})) is finite V44() set
Product (0 |-> m) is complex real ext-real set
m is complex set
(m,1) is complex set
1 |-> m is V1() V4( NAT ) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued 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
<*m*> is V1() V4( NAT ) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued 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
Product <*m*> is complex set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
k is complex set
(k,(m + 1)) is complex set
(m + 1) |-> k is V1() V4( NAT ) Function-like finite m + 1 -element FinSequence-like FinSubsequence-like complex-valued 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
m |-> k is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
<*k*> is V1() V4( NAT ) Function-like non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued 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
(m |-> k) ^ <*k*> is V1() V4( NAT ) Function-like non empty finite m + 1 -element FinSequence-like FinSubsequence-like complex-valued set
Product ((m |-> k) ^ <*k*>) is complex set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m,k) is complex real ext-real set
k |-> m is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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( INT ) V5({m}) Function-like V30( Seg k,{m}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg k),{m}))
{m} is non empty V12() finite V44() 1 -element V61() V62() V63() V64() V65() V66() set
K20((Seg k),{m}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg k),{m})) is finite V44() set
Product (k |-> m) is complex real ext-real set
n is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m,n) is complex real ext-real set
n |-> m is V1() V4( NAT ) Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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
(Seg n) --> m is V1() V4( Seg n) V5( INT ) V5({m}) Function-like V30( Seg n,{m}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg n),{m}))
K20((Seg n),{m}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg n),{m})) is finite V44() set
Product (n |-> m) is complex real ext-real set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(m,(n + 1)) is complex real ext-real set
(n + 1) |-> m is V1() V4( NAT ) Function-like finite n + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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}))
K20((Seg (n + 1)),{m}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg (n + 1)),{m})) is finite V44() set
Product ((n + 1) |-> m) is complex real ext-real set
t is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
t * m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m,0) is complex real ext-real set
0 |-> m is V1() V4( NAT ) V5( RAT ) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite finite-yielding V44() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() set
Seg 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite V44() cardinal 0 -element FinSequence-membered V61() V62() V63() V64() V65() V66() V67() 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 <= 0 ) } is set
(Seg 0) --> m is V1() V4( Seg 0) V5( INT ) V5({m}) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V30( Seg 0,{m}) integer finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() Element of K19(K20((Seg 0),{m}))
K20((Seg 0),{m}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg 0),{m})) is finite V44() set
Product (0 |-> m) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
k is complex set
(k,m) is complex set
m |-> k is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
m |-> (k * n) is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
m |-> n is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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 is complex Element of COMPLEX
(t,m) is complex set
m |-> t is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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 is complex Element of COMPLEX
(t,m) is complex set
m |-> t is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
m |-> (t * t) is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
m + k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
n is complex set
(n,(m + k)) is complex set
(m + k) |-> n is V1() V4( NAT ) Function-like finite m + k -element FinSequence-like FinSubsequence-like complex-valued 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
m |-> n is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
k |-> n is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued 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 is complex Element of COMPLEX
(t,m) is complex set
m |-> t is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
k |-> t is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued 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
(m + k) |-> t is V1() V4( NAT ) V5( COMPLEX ) Function-like finite m + k -element FinSequence-like FinSubsequence-like complex-valued Element of (m + k) -tuples_on COMPLEX
(m + k) -tuples_on COMPLEX is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
COMPLEX * is functional non empty FinSequence-membered FinSequenceSet of COMPLEX
{ 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
K201() is V1() V4(K20(COMPLEX,COMPLEX)) V5( COMPLEX ) Function-like V30(K20(COMPLEX,COMPLEX), COMPLEX ) complex-valued Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))
K258(COMPLEX,((m + k) |-> t),K201()) is complex Element of COMPLEX
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
m * k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
n is complex set
(n,m) is complex set
m |-> n is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
k |-> (n,m) is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued 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
(m * k) |-> n is V1() V4( NAT ) Function-like finite m * k -element FinSequence-like FinSubsequence-like complex-valued 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 is complex Element of COMPLEX
(t,(m * k)) is complex set
(m * k) |-> t is V1() V4( NAT ) Function-like finite m * k -element FinSequence-like FinSubsequence-like complex-valued 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
m |-> t is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued 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
k |-> (t,m) is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued 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
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(1,m) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
m |-> 1 is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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) --> 1 is V1() V4( Seg m) V5( RAT ) V5( INT ) V5({1}) Function-like V30( Seg m,{1}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),{1}))
K20((Seg m),{1}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),{1})) is finite V44() set
Product (m |-> 1) is complex real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(1,k) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
k |-> 1 is V1() V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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) --> 1 is V1() V4( Seg k) V5( RAT ) V5( INT ) V5({1}) 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}))
K20((Seg k),{1}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg k),{1})) is finite V44() set
Product (k |-> 1) is complex real ext-real set
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(1,(k + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
(k + 1) |-> 1 is V1() V4( NAT ) Function-like finite k + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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}))
K20((Seg (k + 1)),{1}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg (k + 1)),{1})) is finite V44() set
Product ((k + 1) |-> 1) is complex real ext-real set
1 * 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(1,0) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
0 |-> 1 is V1() V4( NAT ) V5( RAT ) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite finite-yielding V44() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() set
Seg 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite V44() cardinal 0 -element FinSequence-membered V61() V62() V63() V64() V65() V66() V67() 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 <= 0 ) } is set
(Seg 0) --> 1 is V1() V4( Seg 0) V5( RAT ) V5( INT ) V5({1}) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V30( Seg 0,{1}) integer finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() Element of K19(K20((Seg 0),{1}))
K20((Seg 0),{1}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg 0),{1})) is finite V44() set
Product (0 |-> 1) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(0,m) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
m |-> 0 is V1() empty-yielding V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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) --> 0 is V1() V4( Seg m) V5( RAT ) V5( INT ) V5({0}) Function-like V30( Seg m,{0}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg m),{0}))
{0} is non empty V12() finite V44() 1 -element V61() V62() V63() V64() V65() V66() set
K20((Seg m),{0}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),{0})) is finite V44() set
Product (m |-> 0) is complex real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(0,k) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
k |-> 0 is V1() empty-yielding V4( NAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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) --> 0 is V1() V4( Seg k) V5( RAT ) V5( INT ) V5({0}) Function-like V30( Seg k,{0}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg k),{0}))
K20((Seg k),{0}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg k),{0})) is finite V44() set
Product (k |-> 0) is complex real ext-real set
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
(0,(k + 1)) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
(k + 1) |-> 0 is V1() empty-yielding V4( NAT ) Function-like finite k + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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({0}) Function-like V30( Seg (k + 1),{0}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg (k + 1)),{0}))
K20((Seg (k + 1)),{0}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg (k + 1)),{0})) is finite V44() set
Product ((k + 1) |-> 0) is complex real ext-real set
(0,k) * 0 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
(0,1) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
1 |-> 0 is V1() empty-yielding V4( NAT ) Function-like one-to-one non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V55() decreasing non-decreasing non-increasing set
(Seg 1) --> 0 is V1() V4( Seg 1) V5( RAT ) V5( INT ) V5({0}) Function-like V30( Seg 1,{0}) finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg 1),{0}))
K20((Seg 1),{0}) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg 1),{0})) is finite V44() set
Product (1 |-> 0) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
idseq m is V1() V4( NAT ) Function-like finite m -element FinSequence-like FinSubsequence-like 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)))
K20((Seg m),(Seg m)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),(Seg m))) is finite V44() set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
idseq m is V1() V4( NAT ) V5( RAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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)))
K20((Seg m),(Seg m)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),(Seg m))) is finite V44() set
Product (idseq m) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m) is complex real ext-real Element of REAL
idseq m is V1() V4( NAT ) V5( RAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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)))
K20((Seg m),(Seg m)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),(Seg m))) is finite V44() set
Product (idseq m) is complex real ext-real set
(0) is complex real ext-real Element of REAL
idseq 0 is V1() V4( NAT ) V5( RAT ) Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite finite-yielding V44() cardinal 0 -element FinSequence-like FinSubsequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() set
Seg 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite V44() cardinal 0 -element FinSequence-membered V61() V62() V63() V64() V65() V66() V67() 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 <= 0 ) } is set
id (Seg 0) is V1() V4( Seg 0) V5( RAT ) V5( INT ) V5( Seg 0) functional empty total epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative integer finite finite-yielding V44() cardinal {} -element FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V61() V62() V63() V64() V65() V66() V67() Element of K19(K20((Seg 0),(Seg 0)))
K20((Seg 0),(Seg 0)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg 0),(Seg 0))) is finite V44() set
Product (idseq 0) is complex real ext-real set
(1) is complex real ext-real Element of REAL
Product (idseq 1) is complex real ext-real set
(2) is complex real ext-real Element of REAL
Product (idseq 2) is complex real ext-real set
1 * 2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((m + 1)) is complex real ext-real Element of REAL
idseq (m + 1) is V1() V4( NAT ) V5( RAT ) Function-like finite m + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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
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
idseq m is V1() V4( NAT ) V5( RAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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)))
K20((Seg m),(Seg m)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),(Seg m))) is finite V44() set
Product (idseq m) is complex real ext-real set
(m) * (m + 1) is complex real ext-real Element of REAL
<*(m + 1)*> is V1() V4( NAT ) V5( NAT ) Function-like one-to-one non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V55() decreasing non-decreasing non-increasing FinSequence of NAT
[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
(idseq m) ^ <*(m + 1)*> is V1() V4( NAT ) Function-like non empty finite m + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m) is complex real ext-real Element of REAL
idseq m is V1() V4( NAT ) V5( RAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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)))
K20((Seg m),(Seg m)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),(Seg m))) is finite V44() set
Product (idseq m) is complex real ext-real set
k is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(k) is complex real ext-real Element of REAL
idseq k is V1() V4( NAT ) V5( RAT ) Function-like finite k -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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
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)))
K20((Seg k),(Seg k)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg k),(Seg k))) is finite V44() set
Product (idseq k) is complex real ext-real set
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real ext-real positive non negative integer V35() finite cardinal V61() V62() V63() V64() V65() V66() Element of NAT
((k + 1)) is complex real ext-real Element of REAL
idseq (k + 1) is V1() V4( NAT ) V5( RAT ) Function-like finite k + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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
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
n 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
(k + 1) * n 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
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m) is complex real ext-real Element of REAL
idseq m is V1() V4( NAT ) V5( RAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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)))
K20((Seg m),(Seg m)) is V5( RAT ) V5( INT ) finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg m),(Seg m))) is finite V44() set
Product (idseq m) is complex real ext-real set
m is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal set
(m) is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer finite cardinal Element of REAL
idseq m is V1() V4( NAT ) V5( RAT ) Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued 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