:: UPROOTS semantic presentation

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

{ b

[: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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

F

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