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