REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V83() V288() V289() V291() set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V83() V286() V288() Element of bool REAL
bool REAL is non empty non trivial non finite set
F_Complex is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like V184() V185() V186() V187() algebraic-closed doubleLoopStr
the carrier of F_Complex is non empty non trivial set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V83() set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V33() real Function-yielding finite finite-yielding V41() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V83() FinSequence-yielding finite-support V288() V289() V290() V291() set
omega is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V83() V286() V288() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K102(NAT) is V31() set
COMPLEX is non empty non trivial non finite complex-membered V83() set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V83() set
[:REAL,REAL:] is Relation-like non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty non trivial non finite set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
{{},1} is non empty finite V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
K413() is set
bool K413() is non empty set
K414() is Element of bool K413()
2 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],2:] is Relation-like RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:2,2:],2:] is non empty finite V41() set
[:1,1:] is Relation-like RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is non empty finite V41() set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is non empty finite V41() set
[:[:1,1:],REAL:] is Relation-like non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:[:2,2:],REAL:] is Relation-like non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
K645(2) is V253() L21()
the carrier of K645(2) is set
the carrier of K645(2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K645(2)
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is non empty non trivial non finite set
[:NAT,REAL:] is Relation-like non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty non trivial non finite set
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = 1 } is set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
3 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V33() real Function-yielding finite finite-yielding V41() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() ext-real non positive non negative V54() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V83() FinSequence-yielding finite-support V288() V289() V290() V291() Element of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V33() real Function-yielding finite finite-yielding V41() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V83() FinSequence-yielding finite-support V288() V289() V290() V291() set
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper V33() real Function-yielding finite finite-yielding V41() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V49() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V83() FinSequence-yielding finite-support V288() V289() V290() V291() FinSequence of REAL
Sum (<*> REAL) is V33() real ext-real Element of REAL
K786() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total V32( REAL ) complex-valued ext-real-valued real-valued commutative associative Element of bool [:[:REAL,REAL:],REAL:]
K786() "**" (<*> REAL) is V33() real ext-real Element of REAL
Seg 1 is non empty trivial finite 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of bool NAT
L is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support FinSequence of NAT
dom L is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
Sum L is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
len L is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(len L) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite len L -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support Element of (len L) -tuples_on NAT
(len L) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len L } is set
Seg (len L) is finite len L -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
(Seg (len L)) --> 1 is Relation-like Seg (len L) -defined RAT -valued INT -valued {1} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg (len L)),{1}:]
{1} is non empty trivial finite V41() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
[:(Seg (len L)),{1}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg (len L)),{1}:] is non empty finite V41() set
cL is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cL + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
s is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support FinSequence of NAT
len s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom s is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
Sum s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(len s) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite len s -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support Element of (len s) -tuples_on NAT
(len s) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len s } is set
Seg (len s) is finite len s -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
(Seg (len s)) --> 1 is Relation-like Seg (len s) -defined RAT -valued INT -valued {1} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg (len s)),{1}:]
[:(Seg (len s)),{1}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg (len s)),{1}:] is non empty finite V41() set
x is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support FinSequence of NAT
f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
<*f*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V71() decreasing non-decreasing non-increasing V263() finite-support Element of NAT *
x ^ <*f*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V263() finite-support M24( REAL , NAT )
dom x is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
cs is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
s . cs is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
x . cs is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
len x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
len <*f*> is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
(len x) + (len <*f*>) is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
(len x) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
s . (len s) is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
(len x) |-> 1 is Relation-like NAT -defined REAL -valued Function-like finite len x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support Element of (len x) -tuples_on REAL
(len x) -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 Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of REAL * : len b1 = len x } is set
Seg (len x) is finite len x -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
(Seg (len x)) --> 1 is Relation-like Seg (len x) -defined RAT -valued INT -valued {1} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg (len x)),{1}:]
[:(Seg (len x)),{1}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg (len x)),{1}:] is non empty finite V41() set
cs is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
len cs is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(len cs) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of REAL * : len b1 = len cs } is set
Sum x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(Sum x) + f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
((Sum x) + f) - f is V33() real V49() ext-real Element of REAL
(cL + 1) - f is V33() real V49() ext-real Element of REAL
cs1a is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative set
x . cs1a is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cs1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
x . cs1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cs1 is Relation-like NAT -defined REAL -valued Function-like finite len cs -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support Element of (len cs) -tuples_on REAL
cs1 . cs1a is V33() real ext-real set
g is Relation-like NAT -defined REAL -valued Function-like finite len x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support Element of (len x) -tuples_on REAL
g . cs1a is V33() real ext-real set
Sum cs1 is V33() real ext-real Element of REAL
K786() "**" cs1 is V33() real ext-real Element of REAL
Sum g is V33() real ext-real Element of REAL
K786() "**" g is V33() real ext-real Element of REAL
Sum cs is V33() real ext-real Element of REAL
K786() "**" cs is V33() real ext-real Element of REAL
cL * 1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cL + f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
((cL + 1) - f) + f is V33() real V49() ext-real Element of REAL
(len x) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite len x -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support Element of (len x) -tuples_on NAT
(len x) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len x } is set
cL |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite cL -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support Element of cL -tuples_on NAT
cL -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = cL } is set
Seg cL is finite cL -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
(Seg cL) --> 1 is Relation-like Seg cL -defined RAT -valued INT -valued {1} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg cL),{1}:]
[:(Seg cL),{1}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg cL),{1}:] is non empty finite V41() set
1 |-> 1 is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V71() decreasing non-decreasing non-increasing V263() finite-support Element of 1 -tuples_on NAT
(Seg 1) --> 1 is Relation-like Seg 1 -defined RAT -valued INT -valued {1} -valued Function-like non empty total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg 1),{1}:]
[:(Seg 1),{1}:] is Relation-like RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg 1),{1}:] is non empty finite V41() set
(cL |-> 1) ^ (1 |-> 1) is Relation-like NAT -defined REAL -valued Function-like non empty finite cL + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V263() finite-support M24( REAL , NAT )
cL + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
<*1*> is Relation-like NAT -defined NAT -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V71() decreasing non-decreasing non-increasing V263() finite-support Element of NAT *
(cL |-> 1) ^ <*1*> is Relation-like NAT -defined REAL -valued Function-like non empty finite cL + 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V263() finite-support M24( REAL , NAT )
cL is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support FinSequence of NAT
len cL is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom cL is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
Sum cL is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(len cL) |-> 1 is Relation-like NAT -defined NAT -valued Function-like finite len cL -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued V263() finite-support Element of (len cL) -tuples_on NAT
(len cL) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len cL } is set
Seg (len cL) is finite len cL -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
(Seg (len cL)) --> 1 is Relation-like Seg (len cL) -defined RAT -valued INT -valued {1} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg (len cL)),{1}:]
[:(Seg (len cL)),{1}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg (len cL)),{1}:] is non empty finite V41() set
F1() is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative set
L is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative set
1 - 1 is V33() real V49() ext-real Element of REAL
L - 1 is V33() real V49() ext-real Element of REAL
(L - 1) + 1 is V33() real V49() ext-real Element of REAL
L + 0 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative set
cL is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cL + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
L is non empty left_add-cancelable right_add-cancelable right_complementable add-associative right_zeroed V184() V185() V186() V187() addLoopStr
the carrier of L is non empty set
0. L is V107(L) Element of the carrier of L
the ZeroF of L is Element of the carrier of L
cL is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
len cL is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom cL is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
Sum cL is Element of the carrier of L
cL /. 1 is Element of the carrier of L
cL /. 2 is Element of the carrier of L
(cL /. 1) + (cL /. 2) is Element of the carrier of L
cL . 1 is set
s is Element of the carrier of L
<*s*> is Relation-like NAT -defined the carrier of L -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
the carrier of L * is functional non empty FinSequence-membered FinSequenceSet of the carrier of L
x is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
<*s*> ^ x is Relation-like NAT -defined the carrier of L -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
len <*s*> is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
cL . 2 is set
2 - 1 is V33() real V49() ext-real Element of REAL
x . (2 - 1) is set
x . 1 is set
len x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
1 + (len x) is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
f is Element of the carrier of L
<*f*> is Relation-like NAT -defined the carrier of L -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of the carrier of L *
cs is Relation-like NAT -defined the carrier of L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
<*f*> ^ cs is Relation-like NAT -defined the carrier of L -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of L
len <*f*> is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
cs1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom cs is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
1 + cs1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
dom x is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
1 + (1 + cs1) is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
cs . cs1 is set
x . (1 + cs1) is set
cL . (1 + (1 + cs1)) is set
Sum x is Element of the carrier of L
s + (Sum x) is Element of the carrier of L
Sum cs is Element of the carrier of L
f + (Sum cs) is Element of the carrier of L
s + (f + (Sum cs)) is Element of the carrier of L
f + (0. L) is Element of the carrier of L
s + (f + (0. L)) is Element of the carrier of L
s + f is Element of the carrier of L
(cL /. 1) + f is Element of the carrier of L
L is finite set
card L is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
x is set
x `2 is set
choose (x `2) is Element of x `2
{(choose (x `2))} is non empty trivial finite 1 -element set
(x `2) \ {(choose (x `2))} is Element of bool (x `2)
bool (x `2) is non empty set
[(choose (x `2)),((x `2) \ {(choose (x `2))})] is V22() set
{(choose (x `2)),((x `2) \ {(choose (x `2))})} is non empty finite set
{{(choose (x `2)),((x `2) \ {(choose (x `2))})},{(choose (x `2))}} is non empty finite V41() set
choose L is Element of L
{(choose L)} is non empty trivial finite 1 -element set
L \ {(choose L)} is finite Element of bool L
bool L is non empty finite V41() set
[(choose L),(L \ {(choose L)})] is V22() set
{(choose L),(L \ {(choose L)})} is non empty finite set
{{(choose L),(L \ {(choose L)})},{(choose L)}} is non empty finite V41() set
s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
s . 1 is set
dom s is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
[:L,(bool L):] is Relation-like finite set
x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
s . x is set
(s . x) `2 is set
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
s . (x + 1) is set
(s . (x + 1)) `2 is set
choose ((s . x) `2) is Element of (s . x) `2
{(choose ((s . x) `2))} is non empty trivial finite 1 -element set
((s . x) `2) \ {(choose ((s . x) `2))} is Element of bool ((s . x) `2)
bool ((s . x) `2) is non empty set
[(choose ((s . x) `2)),(((s . x) `2) \ {(choose ((s . x) `2))})] is V22() set
{(choose ((s . x) `2)),(((s . x) `2) \ {(choose ((s . x) `2))})} is non empty finite set
{{(choose ((s . x) `2)),(((s . x) `2) \ {(choose ((s . x) `2))})},{(choose ((s . x) `2))}} is non empty finite V41() set
f is finite set
card f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card f) + x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
f is set
cs is set
[f,cs] is V22() set
{f,cs} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,cs},{f}} is non empty finite V41() set
cs1 is finite set
card cs1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card cs1) + x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cs1 is finite set
card cs1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card cs1) + x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
g is finite set
card g is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card g) + (x + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
{(choose ((s . x) `2))} \/ (((s . x) `2) \ {(choose ((s . x) `2))}) is non empty set
(card g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
(s . 1) `2 is set
x is finite set
card x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card x) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
{(choose L)} \/ (L \ {(choose L)}) is non empty finite set
proj2 s is finite set
x is set
f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative set
s . f is set
x is Relation-like NAT -defined [:L,(bool L):] -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of [:L,(bool L):]
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom f is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
dom x is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
proj2 f is finite set
cs is set
cs1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative set
f . cs1 is set
x . cs1 is set
(x . cs1) `1 is set
cs is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
rng cs is finite Element of bool L
len x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
g is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
Seg g is finite g -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
cs | (Seg g) is Relation-like NAT -defined Seg g -defined NAT -defined L -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,L:]
[:NAT,L:] is Relation-like set
bool [:NAT,L:] is non empty set
rng (cs | (Seg g)) is finite Element of bool L
x . g is set
(x . g) `2 is set
(rng (cs | (Seg g))) \/ ((x . g) `2) is set
g + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
Seg (g + 1) is non empty finite g + 1 -element g + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of bool NAT
g + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
cs | (Seg (g + 1)) is Relation-like NAT -defined Seg (g + 1) -defined NAT -defined L -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,L:]
rng (cs | (Seg (g + 1))) is finite Element of bool L
x . (g + 1) is set
(x . (g + 1)) `2 is set
(rng (cs | (Seg (g + 1)))) \/ ((x . (g + 1)) `2) is set
choose ((x . g) `2) is Element of (x . g) `2
{(choose ((x . g) `2))} is non empty trivial finite 1 -element set
((x . g) `2) \ {(choose ((x . g) `2))} is Element of bool ((x . g) `2)
bool ((x . g) `2) is non empty set
[(choose ((x . g) `2)),(((x . g) `2) \ {(choose ((x . g) `2))})] is V22() set
{(choose ((x . g) `2)),(((x . g) `2) \ {(choose ((x . g) `2))})} is non empty finite set
{{(choose ((x . g) `2)),(((x . g) `2) \ {(choose ((x . g) `2))})},{(choose ((x . g) `2))}} is non empty finite V41() set
cs1a is finite set
card cs1a is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card cs1a) + g is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cs1a is finite set
card cs1a is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card cs1a) + g is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
{(choose ((x . g) `2))} \/ (((x . g) `2) \ {(choose ((x . g) `2))}) is non empty set
len cs is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
s1 is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
t is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
p1 is Element of L
<*p1*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
t ^ <*p1*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
dom cs is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
rng s1 is finite Element of bool L
rng t is finite Element of bool L
proj2 <*p1*> is non empty trivial finite 1 -element set
(rng t) \/ (proj2 <*p1*>) is non empty finite set
{p1} is non empty trivial finite 1 -element set
(rng t) \/ {p1} is non empty finite set
cs . (g + 1) is set
s1 . (g + 1) is set
len t is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(x . (g + 1)) `1 is set
((x . g) `2) \ {p1} is Element of bool ((x . g) `2)
f1 is finite set
card f1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card f1) + g is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cs1 is finite set
card cs1 is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card cs1) + (g + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
(card cs1) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
len cs is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom cs is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
cs | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined L -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,L:]
[:NAT,L:] is Relation-like set
bool [:NAT,L:] is non empty set
rng (cs | (Seg 1)) is finite Element of bool L
x . 1 is set
(x . 1) `2 is set
(rng (cs | (Seg 1))) \/ ((x . 1) `2) is set
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
Seg (0 + 1) is non empty finite 0 + 1 -element 0 + 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of bool NAT
cs1a is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
cs1a . 1 is set
cs . 1 is set
(x . 1) `1 is set
<*(choose L)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
cs1 is Element of L
<*cs1*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
g is finite set
card g is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
{(choose L)} \/ (L \ {(choose L)}) is non empty finite set
x . (len cs) is set
(x . (len cs)) `2 is set
g is finite set
card g is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
(card g) + (len x) is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
Seg (len cs) is finite len cs -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
cs | (Seg (len cs)) is Relation-like NAT -defined Seg (len cs) -defined NAT -defined L -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT,L:]
(rng cs) \/ ((x . (len cs)) `2) is set
L is finite set
the Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
L is finite set
(L) is Relation-like NAT -defined L -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
the Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
L is finite set
(L) is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
the Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
len (L) is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
card L is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
rng (L) is finite Element of bool L
bool L is non empty finite V41() set
L is non empty finite set
(L) is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
the Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
len (L) is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
card L is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of omega
L is set
{L} is non empty trivial finite 1 -element set
({L}) is Relation-like NAT -defined {L} -valued Function-like one-to-one non empty onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of {L}
the Relation-like NAT -defined {L} -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of {L} is Relation-like NAT -defined {L} -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of {L}
<*L*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
rng ({L}) is non empty trivial finite 1 -element Element of bool {L}
bool {L} is non empty finite V41() set
len ({L}) is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of NAT
card {L} is epsilon-transitive epsilon-connected ordinal natural non empty V33() real finite cardinal V49() ext-real positive non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() Element of omega
L is finite set
(L) is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
the Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L is Relation-like NAT -defined L -valued Function-like one-to-one onto bijective finite FinSequence-like FinSubsequence-like finite-support FinSequence of L
(L) " is Relation-like Function-like one-to-one set
card L is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of omega
Seg (card L) is finite card L -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
[:L,(Seg (card L)):] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:L,(Seg (card L)):] is non empty finite V41() set
len (L) is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom (L) is finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of bool NAT
proj2 ((L) ") is set
rng (L) is finite Element of bool L
bool L is non empty finite V41() set
proj1 ((L) ") is set
L is set
bool L is non empty set
EmptyBag L is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
Bags L is non empty set
Bags L is functional non empty Element of bool (Bags L)
bool (Bags L) is non empty set
cL is finite Element of bool L
s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cL --> s is Relation-like cL -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:cL,NAT:]
[:cL,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:cL,NAT:] is non empty set
{s} is non empty trivial finite V41() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
[:cL,{s}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
(EmptyBag L) +* (cL --> s) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
L --> 0 is Relation-like L -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:L,NAT:]
[:L,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:L,NAT:] is non empty set
{0} is functional non empty trivial finite V41() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
[:L,{0}:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
dom (cL --> s) is finite Element of bool cL
bool cL is non empty finite V41() set
f is set
((EmptyBag L) +* (cL --> s)) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(EmptyBag L) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
f is set
((EmptyBag L) +* (cL --> s)) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(cL --> s) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
support ((EmptyBag L) +* (cL --> s)) is set
f is set
((EmptyBag L) +* (cL --> s)) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
f is set
((EmptyBag L) +* (cL --> s)) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(cL --> s) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
f is set
((EmptyBag L) +* (cL --> s)) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
cs is set
((EmptyBag L) +* (cL --> s)) . cs is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
proj1 ((EmptyBag L) +* (cL --> s)) is set
dom (EmptyBag L) is Element of bool L
(dom (EmptyBag L)) \/ (dom (cL --> s)) is set
L \/ (dom (cL --> s)) is set
L \/ cL is set
L is set
bool L is non empty set
cL is finite Element of bool L
s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(L,cL,s) is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
Bags L is non empty set
Bags L is functional non empty Element of bool (Bags L)
bool (Bags L) is non empty set
EmptyBag L is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
cL --> s is Relation-like cL -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:cL,NAT:]
[:cL,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:cL,NAT:] is non empty set
{s} is non empty trivial finite V41() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
[:cL,{s}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
(EmptyBag L) +* (cL --> s) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
x is set
(L,cL,s) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom (cL --> s) is finite Element of bool cL
bool cL is non empty finite V41() set
(EmptyBag L) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
L is set
bool L is non empty set
cL is finite Element of bool L
s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(L,cL,s) is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
Bags L is non empty set
Bags L is functional non empty Element of bool (Bags L)
bool (Bags L) is non empty set
EmptyBag L is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
cL --> s is Relation-like cL -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:cL,NAT:]
[:cL,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:cL,NAT:] is non empty set
{s} is non empty trivial finite V41() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
[:cL,{s}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
(EmptyBag L) +* (cL --> s) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
x is set
(L,cL,s) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
dom (cL --> s) is finite Element of bool cL
bool cL is non empty finite V41() set
(cL --> s) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
L is set
bool L is non empty set
cL is finite Element of bool L
s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(L,cL,s) is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
Bags L is non empty set
Bags L is functional non empty Element of bool (Bags L)
bool (Bags L) is non empty set
EmptyBag L is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
cL --> s is Relation-like cL -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:cL,NAT:]
[:cL,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:cL,NAT:] is non empty set
{s} is non empty trivial finite V41() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
[:cL,{s}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
(EmptyBag L) +* (cL --> s) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
support (L,cL,s) is finite set
x is set
(L,cL,s) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
f is set
(L,cL,s) . f is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
L is set
bool L is non empty set
EmptyBag L is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
Bags L is non empty set
Bags L is functional non empty Element of bool (Bags L)
bool (Bags L) is non empty set
cL is finite Element of bool L
s is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(L,cL,s) is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
cL --> s is Relation-like cL -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:cL,NAT:]
[:cL,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:cL,NAT:] is non empty set
{s} is non empty trivial finite V41() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V286() V287() V288() V289() V290() set
[:cL,{s}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
(EmptyBag L) +* (cL --> s) is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
x is set
(L,cL,s) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(EmptyBag L) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(L,cL,s) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(EmptyBag L) . x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
L is set
bool L is non empty set
cL is finite Element of bool L
s is finite Element of bool L
cL \/ s is finite Element of bool L
x is epsilon-transitive epsilon-connected ordinal natural V33() real finite cardinal V49() ext-real non negative V54() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V288() V289() V290() Element of NAT
(L,(cL \/ s),x) is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
Bags L is non empty set
Bags L is functional non empty Element of bool (Bags L)
bool (Bags L) is non empty set
EmptyBag L is Relation-like L -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support Element of Bags L
(cL \/ s) --> x is Relation-like cL \/ s -defined NAT -valued RAT -valued INT -valued Function-like total quasi_total finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(cL \/ s),NAT:]
[:(cL \/ s),NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:(cL \/ s),NAT:] is non empty set
{x} is non empty trivial finite