:: GROEB_2 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V29() V30() Element of K19(REAL)

K19(REAL) is set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V29() V30() set

K19(omega) is non trivial non finite set

K19(NAT) is non trivial non finite set

COMPLEX is set

RAT is set

INT is set

{} is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V28() V29() V31( {} ) FinSequence-membered V52() V53() complex ext-real non positive non negative set

1 is non empty epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real positive non negative Element of NAT

{{},1} is non empty finite V28() set

2 is non empty epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real positive non negative Element of NAT

K20(COMPLEX,COMPLEX) is set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is non trivial non finite set

K20(K20(NAT,NAT),NAT) is non trivial non finite set

K19(K20(K20(NAT,NAT),NAT)) is non trivial non finite set

K20(NAT,REAL) is set

K19(K20(NAT,REAL)) is set

3 is non empty epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real positive non negative Element of NAT

Seg 1 is non empty trivial finite V31(1) Element of K19(NAT)

{1} is non empty trivial finite V28() V31(1) set

Seg 2 is non empty finite V31(2) Element of K19(NAT)

{1,2} is non empty finite V28() set

0 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V28() V29() V31( {} ) FinSequence-membered V52() V53() complex ext-real non positive non negative Element of NAT

n is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of n is non empty set

0. n is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

the ZeroF of n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

T is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

dom T is finite Element of K19(NAT)

Sum T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

L is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

T | L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (T | L) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real positive non negative Element of NAT

dom P is finite Element of K19(NAT)

A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

Seg (P + 1) is non empty finite V31(P + 1) V31(P + 1) Element of K19(NAT)

P + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real positive non negative Element of NAT

Seg P is finite V31(P) Element of K19(NAT)

P | (Seg P) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSubsequence-like finite-support Element of K19(K20(NAT, the carrier of n))

K20(NAT, the carrier of n) is non trivial non finite set

K19(K20(NAT, the carrier of n)) is non trivial non finite set

m is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len m is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

dom m is finite Element of K19(NAT)

P | P is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

P /. (P + 1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

<*(P /. (P + 1))*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support M29( the carrier of n,K500( the carrier of n))

K500( the carrier of n) is functional non empty FinSequence-membered M28( the carrier of n)

m ^ <*(P /. (P + 1))*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

P . (P + 1) is set

<*(P . (P + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support set

m ^ <*(P . (P + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

P | A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

dom (P | A) is finite Element of K19(NAT)

Seg A is finite V31(A) Element of K19(NAT)

P | (Seg A) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSubsequence-like finite-support Element of K19(K20(NAT, the carrier of n))

dom (P | (Seg A)) is finite Element of K19(NAT)

p is set

s is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(dom P) /\ (Seg A) is finite Element of K19(NAT)

p is set

(P | (Seg A)) . p is set

P . p is set

p is set

Sum (P | A) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

Sum P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

p is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P . p is set

m . p is set

m /. p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P /. p is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

Sum P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

Sum m is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

Sum <*(P /. (P + 1))*> is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

(Sum m) + (Sum <*(P /. (P + 1))*>) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

(Sum m) + (P /. (P + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

m | A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (m | A) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P | A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (P | A) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P | A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (P | A) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

Sum P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P | A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (P | A) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

Sum P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

dom P is finite Element of K19(NAT)

A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

Sum P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P | A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (P | A) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

len P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

dom P is finite Element of K19(NAT)

P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

Sum P is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

P | P is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (P | P) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

len T is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is non empty Abelian add-associative right_zeroed addLoopStr

the carrier of n is non empty set

T is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum T is Element of the carrier of n

L is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

Swap (T,L,P) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (Swap (T,L,P)) is Element of the carrier of n

len T is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

len T is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

Seg (len T) is finite V31( len T) Element of K19(NAT)

dom T is finite Element of K19(NAT)

L -' 1 is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

T | (L -' 1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

T /. P is Element of the carrier of n

<*(T /. P)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support M29( the carrier of n,K500( the carrier of n))

K500( the carrier of n) is functional non empty FinSequence-membered M28( the carrier of n)

(T | (L -' 1)) ^ <*(T /. P)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

P -' L is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(P -' L) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

T /^ L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

(T /^ L) | ((P -' L) -' 1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

T /. L is Element of the carrier of n

<*(T /. L)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support M29( the carrier of n,K500( the carrier of n))

(((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. L)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

T /^ P is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

((((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. L)*>) ^ (T /^ P) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum ((((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. L)*>) is Element of the carrier of n

Sum (T /^ P) is Element of the carrier of n

(Sum ((((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. L)*>)) + (Sum (T /^ P)) is Element of the carrier of n

Sum (((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

Sum <*(T /. L)*> is Element of the carrier of n

(Sum (((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. L)*>) is Element of the carrier of n

((Sum (((T | (L -' 1)) ^ <*(T /. P)*>) ^ ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. L)*>)) + (Sum (T /^ P)) is Element of the carrier of n

Sum ((T | (L -' 1)) ^ <*(T /. P)*>) is Element of the carrier of n

Sum ((T /^ L) | ((P -' L) -' 1)) is Element of the carrier of n

(Sum ((T | (L -' 1)) ^ <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

((Sum ((T | (L -' 1)) ^ <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. L)*>) is Element of the carrier of n

(((Sum ((T | (L -' 1)) ^ <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. L)*>)) + (Sum (T /^ P)) is Element of the carrier of n

Sum (T | (L -' 1)) is Element of the carrier of n

Sum <*(T /. P)*> is Element of the carrier of n

(Sum (T | (L -' 1))) + (Sum <*(T /. P)*>) is Element of the carrier of n

((Sum (T | (L -' 1))) + (Sum <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

(((Sum (T | (L -' 1))) + (Sum <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. L)*>) is Element of the carrier of n

((((Sum (T | (L -' 1))) + (Sum <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. L)*>)) + (Sum (T /^ P)) is Element of the carrier of n

((Sum (T | (L -' 1))) + (Sum <*(T /. P)*>)) + (Sum <*(T /. L)*>) is Element of the carrier of n

(((Sum (T | (L -' 1))) + (Sum <*(T /. P)*>)) + (Sum <*(T /. L)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

((((Sum (T | (L -' 1))) + (Sum <*(T /. P)*>)) + (Sum <*(T /. L)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum (T /^ P)) is Element of the carrier of n

(Sum (T | (L -' 1))) + (Sum <*(T /. L)*>) is Element of the carrier of n

((Sum (T | (L -' 1))) + (Sum <*(T /. L)*>)) + (Sum <*(T /. P)*>) is Element of the carrier of n

(((Sum (T | (L -' 1))) + (Sum <*(T /. L)*>)) + (Sum <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

((((Sum (T | (L -' 1))) + (Sum <*(T /. L)*>)) + (Sum <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum (T /^ P)) is Element of the carrier of n

(T | (L -' 1)) ^ <*(T /. L)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum ((T | (L -' 1)) ^ <*(T /. L)*>) is Element of the carrier of n

(Sum ((T | (L -' 1)) ^ <*(T /. L)*>)) + (Sum <*(T /. P)*>) is Element of the carrier of n

((Sum ((T | (L -' 1)) ^ <*(T /. L)*>)) + (Sum <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

(((Sum ((T | (L -' 1)) ^ <*(T /. L)*>)) + (Sum <*(T /. P)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum (T /^ P)) is Element of the carrier of n

(Sum ((T | (L -' 1)) ^ <*(T /. L)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

((Sum ((T | (L -' 1)) ^ <*(T /. L)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. P)*>) is Element of the carrier of n

(((Sum ((T | (L -' 1)) ^ <*(T /. L)*>)) + (Sum ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. P)*>)) + (Sum (T /^ P)) is Element of the carrier of n

((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) is Element of the carrier of n

(Sum (((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. P)*>) is Element of the carrier of n

((Sum (((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1)))) + (Sum <*(T /. P)*>)) + (Sum (T /^ P)) is Element of the carrier of n

(((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. P)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum ((((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. P)*>) is Element of the carrier of n

(Sum ((((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. P)*>)) + (Sum (T /^ P)) is Element of the carrier of n

((((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. P)*>) ^ (T /^ P) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (((((T | (L -' 1)) ^ <*(T /. L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. P)*>) ^ (T /^ P)) is Element of the carrier of n

T . L is set

<*(T . L)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support set

(T | (L -' 1)) ^ <*(T . L)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

((T | (L -' 1)) ^ <*(T . L)*>) ^ ((T /^ L) | ((P -' L) -' 1)) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

(((T | (L -' 1)) ^ <*(T . L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. P)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

((((T | (L -' 1)) ^ <*(T . L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T /. P)*>) ^ (T /^ P) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

T . P is set

<*(T . P)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support set

(((T | (L -' 1)) ^ <*(T . L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T . P)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

((((T | (L -' 1)) ^ <*(T . L)*>) ^ ((T /^ L) | ((P -' L) -' 1))) ^ <*(T . P)*>) ^ (T /^ P) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

Swap (T,P,L) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

P -' 1 is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

T | (P -' 1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

T /. L is Element of the carrier of n

<*(T /. L)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support M29( the carrier of n,K500( the carrier of n))

K500( the carrier of n) is functional non empty FinSequence-membered M28( the carrier of n)

(T | (P -' 1)) ^ <*(T /. L)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

L -' P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(L -' P) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

T /^ P is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

(T /^ P) | ((L -' P) -' 1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

T /. P is Element of the carrier of n

<*(T /. P)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support M29( the carrier of n,K500( the carrier of n))

(((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. P)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

T /^ L is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

((((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. P)*>) ^ (T /^ L) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (Swap (T,P,L)) is Element of the carrier of n

Sum ((((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. P)*>) is Element of the carrier of n

Sum (T /^ L) is Element of the carrier of n

(Sum ((((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. P)*>)) + (Sum (T /^ L)) is Element of the carrier of n

Sum (((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

Sum <*(T /. P)*> is Element of the carrier of n

(Sum (((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. P)*>) is Element of the carrier of n

((Sum (((T | (P -' 1)) ^ <*(T /. L)*>) ^ ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. P)*>)) + (Sum (T /^ L)) is Element of the carrier of n

Sum ((T | (P -' 1)) ^ <*(T /. L)*>) is Element of the carrier of n

Sum ((T /^ P) | ((L -' P) -' 1)) is Element of the carrier of n

(Sum ((T | (P -' 1)) ^ <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

((Sum ((T | (P -' 1)) ^ <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. P)*>) is Element of the carrier of n

(((Sum ((T | (P -' 1)) ^ <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. P)*>)) + (Sum (T /^ L)) is Element of the carrier of n

Sum (T | (P -' 1)) is Element of the carrier of n

Sum <*(T /. L)*> is Element of the carrier of n

(Sum (T | (P -' 1))) + (Sum <*(T /. L)*>) is Element of the carrier of n

((Sum (T | (P -' 1))) + (Sum <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

(((Sum (T | (P -' 1))) + (Sum <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. P)*>) is Element of the carrier of n

((((Sum (T | (P -' 1))) + (Sum <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. P)*>)) + (Sum (T /^ L)) is Element of the carrier of n

((Sum (T | (P -' 1))) + (Sum <*(T /. L)*>)) + (Sum <*(T /. P)*>) is Element of the carrier of n

(((Sum (T | (P -' 1))) + (Sum <*(T /. L)*>)) + (Sum <*(T /. P)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

((((Sum (T | (P -' 1))) + (Sum <*(T /. L)*>)) + (Sum <*(T /. P)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum (T /^ L)) is Element of the carrier of n

(Sum (T | (P -' 1))) + (Sum <*(T /. P)*>) is Element of the carrier of n

((Sum (T | (P -' 1))) + (Sum <*(T /. P)*>)) + (Sum <*(T /. L)*>) is Element of the carrier of n

(((Sum (T | (P -' 1))) + (Sum <*(T /. P)*>)) + (Sum <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

((((Sum (T | (P -' 1))) + (Sum <*(T /. P)*>)) + (Sum <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum (T /^ L)) is Element of the carrier of n

(T | (P -' 1)) ^ <*(T /. P)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum ((T | (P -' 1)) ^ <*(T /. P)*>) is Element of the carrier of n

(Sum ((T | (P -' 1)) ^ <*(T /. P)*>)) + (Sum <*(T /. L)*>) is Element of the carrier of n

((Sum ((T | (P -' 1)) ^ <*(T /. P)*>)) + (Sum <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

(((Sum ((T | (P -' 1)) ^ <*(T /. P)*>)) + (Sum <*(T /. L)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum (T /^ L)) is Element of the carrier of n

(Sum ((T | (P -' 1)) ^ <*(T /. P)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

((Sum ((T | (P -' 1)) ^ <*(T /. P)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. L)*>) is Element of the carrier of n

(((Sum ((T | (P -' 1)) ^ <*(T /. P)*>)) + (Sum ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. L)*>)) + (Sum (T /^ L)) is Element of the carrier of n

((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) is Element of the carrier of n

(Sum (((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. L)*>) is Element of the carrier of n

((Sum (((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1)))) + (Sum <*(T /. L)*>)) + (Sum (T /^ L)) is Element of the carrier of n

(((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. L)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum ((((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. L)*>) is Element of the carrier of n

(Sum ((((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. L)*>)) + (Sum (T /^ L)) is Element of the carrier of n

((((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. L)*>) ^ (T /^ L) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of n

Sum (((((T | (P -' 1)) ^ <*(T /. P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. L)*>) ^ (T /^ L)) is Element of the carrier of n

T . P is set

<*(T . P)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support set

(T | (P -' 1)) ^ <*(T . P)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

((T | (P -' 1)) ^ <*(T . P)*>) ^ ((T /^ P) | ((L -' P) -' 1)) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

(((T | (P -' 1)) ^ <*(T . P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. L)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

((((T | (P -' 1)) ^ <*(T . P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T /. L)*>) ^ (T /^ L) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

T . L is set

<*(T . L)*> is Relation-like NAT -defined Function-like constant non empty trivial finite V31(1) FinSequence-like FinSubsequence-like finite-support set

(((T | (P -' 1)) ^ <*(T . P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T . L)*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

((((T | (P -' 1)) ^ <*(T . P)*>) ^ ((T /^ P) | ((L -' P) -' 1))) ^ <*(T . L)*>) ^ (T /^ L) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

len T is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L + P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L + P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

A is set

dom P is Element of K19(n)

K19(n) is set

P . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(L . A) + (P . A) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

((L . A) + (P . A)) -' (L . A) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

T . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T . A) -' (L . A) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(L . A) + (P . A) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

((L . A) + (P . A)) -' (L . A) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

dom P is Element of K19(n)

n is set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is Relation-like Function-like set

dom P is set

A is set

P is Relation-like n -defined Function-like total set

rng P is set

dom P is Element of K19(n)

K19(n) is set

i is set

P . i is set

T . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . i),(L . i)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

support P is set

A is set

P . A is set

support T is finite set

support L is finite set

(support T) \/ (support L) is finite set

L . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . A),(L . A)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

A is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

dom A is Element of K19(n)

dom L is Element of K19(n)

dom T is Element of K19(n)

i is set

A . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . i),(L . i)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

i is set

T . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

A . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . i),(L . i)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

i is set

A . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . i),(L . i)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

i is set

A . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . i),(L . i)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

i is set

A . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . i),(L . i)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

A is set

dom P is Element of K19(n)

K19(n) is set

P . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . A),(L . A)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P . A is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

dom P is Element of K19(n)

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

A is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

i is set

P . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

A . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

P . i is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((A . i),(P . i)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((P . P),(P . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is set

n is set

n is set

n is set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,T,L) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(n,T,L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

P is set

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(n,T,L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

n is set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,T,L) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(n,T,L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

n is set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,T,L) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

T + L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

(n,T,L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T . P) + (L . P) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(T . P) + 0 is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T . P) + (L . P) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

0 + (L . P) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

P is set

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

0 + (L . P) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is set

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T . P) + 0 is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is set

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

P is set

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(T + L) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is set

EmptyBag n is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support Element of Bags n

Bags n is non empty set

Bags n is functional non empty Element of K19((Bags n))

K19((Bags n)) is set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,T,T) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

T + (EmptyBag n) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

n is set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,T,L) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(L . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,L,P) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,L,T) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

(n,L,T) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(n,L,P) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((L . P),(P . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

max ((L . P),(T . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,L,T) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,L,P) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,T,P) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

(n,T,P) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(n,L,P) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((L . P),(P . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

(n,L,T) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((L . P),(T . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

max ((T . P),(P . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is set

T is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,T,P) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

L is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

(n,L,P) is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

P is set

T . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(n,L,P) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

(n,T,P) . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

P . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((T . P),(P . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

L . P is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative V233() Element of NAT

max ((L . P),(P . P)) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative Element of NAT

Bags n is functional non empty Element of K19((Bags n))

Bags n is non empty set

K19((Bags n)) is set

K20((Bags n),(Bags n)) is set

K19(K20((Bags n),(Bags n))) is set

K19((Bags n)) is set

T is Relation-like Bags n -defined Bags n -valued total V46( Bags n, Bags n) reflexive antisymmetric connected transitive V283() admissible Element of K19(K20((Bags n),(Bags n)))

L is functional non empty Element of K19((Bags n))

RelStr(# (Bags n),T #) is non empty strict total reflexive transitive antisymmetric V181() V255() RelStr

MinElement (L,RelStr(# (Bags n),T #)) is Element of the carrier of RelStr(# (Bags n),T #)

the carrier of RelStr(# (Bags n),T #) is non empty set

field T is set

the InternalRel of RelStr(# (Bags n),T #) is Relation-like the carrier of RelStr(# (Bags n),T #) -defined the carrier of RelStr(# (Bags n),T #) -valued total V46( the carrier of RelStr(# (Bags n),T #), the carrier of RelStr(# (Bags n),T #)) reflexive antisymmetric transitive Element of K19(K20( the carrier of RelStr(# (Bags n),T #), the carrier of RelStr(# (Bags n),T #)))

K20( the carrier of RelStr(# (Bags n),T #), the carrier of RelStr(# (Bags n),T #)) is set

K19(K20( the carrier of RelStr(# (Bags n),T #), the carrier of RelStr(# (Bags n),T #))) is set

A is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

[A,A] is V21() set

i is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

[i,i] is V21() set

[i,A] is V21() set

[A,i] is V21() set

n is non empty non trivial left_add-cancelable right_add-cancelable add-cancelable right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like addLoopStr

the carrier of n is non empty non trivial set

T is non zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

- T is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

0. n is zero left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

the ZeroF of n is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

- (- T) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of n

n is set

Bags n is functional non empty Element of K19((Bags n))

Bags n is non empty set

K19((Bags n)) is set

T is non empty left_add-cancelable right_add-cancelable add-cancelable right-distributive left-distributive distributive right_zeroed left_zeroed doubleLoopStr

the carrier of T is non empty set

K20((Bags n), the carrier of T) is set

K19(K20((Bags n), the carrier of T)) is set

L is Relation-like Bags n -defined the carrier of T -valued Function-like non empty total V46( Bags n, the carrier of T) monomial-like V293( Bags n,T) Element of K19(K20((Bags n), the carrier of T))

P is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * L is Relation-like Bags n -defined the carrier of T -valued Function-like non empty total V46( Bags n, the carrier of T) V293( Bags n,T) Element of K19(K20((Bags n), the carrier of T))

Support L is functional Element of K19((Bags n))

K19((Bags n)) is set

Support (P * L) is functional Element of K19((Bags n))

the Relation-like n -defined Function-like Element of Support (P * L) is Relation-like n -defined Function-like Element of Support (P * L)

i is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support Element of Bags n

(P * L) . i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

L . i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * (L . i) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

0. T is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * (0. T) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

Support L is functional Element of K19((Bags n))

K19((Bags n)) is set

A is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

{A} is functional non empty trivial finite V31(1) set

A is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support set

{A} is functional non empty trivial finite V31(1) set

0. T is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

Support (P * L) is functional Element of K19((Bags n))

the Relation-like n -defined Function-like Element of Support (P * L) is Relation-like n -defined Function-like Element of Support (P * L)

p is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support Element of Bags n

(P * L) . p is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

L . p is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * (L . p) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

0. T is zero left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

the ZeroF of T is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

m is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support Element of Bags n

i is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support Element of Bags n

L . m is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

(P * L) . m is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * (L . m) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

L . i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * (L . i) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

Support (P * L) is functional Element of K19((Bags n))

the Relation-like n -defined Function-like Element of Support (P * L) is Relation-like n -defined Function-like Element of Support (P * L)

p is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support Element of Bags n

(P * L) . p is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

L . i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * (L . i) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

m is set

Support (P * L) is functional Element of K19((Bags n))

p is Relation-like n -defined RAT -valued Function-like total V234() V235() V236() V237() finite-support Element of Bags n

(P * L) . p is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

{i} is functional non empty trivial finite V31(1) set

m is set

(P * L) . i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

L . i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

P * (L . i) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of T

Support (P * L) is functional Element of K19((Bags n))

{i} is functional non empty trivial finite V31(1) set

L