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

K19(omega) is non trivial non finite set
K19(NAT) is non trivial non finite set

RAT is set
INT is set

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

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

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

the carrier of n is non empty set

dom T is finite Element of K19(NAT)

dom P is finite Element of K19(NAT)

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

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

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

dom m is finite Element of K19(NAT)

<*(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)

P . (P + 1) is set

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

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

(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

P . p is set
m . p is set

(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

dom P is finite Element of K19(NAT)

dom P is finite Element of K19(NAT)

the carrier of n is non empty set

Sum T is Element of the carrier of n

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

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

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

(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 | (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 -' 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 | (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 /. 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

(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 | (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 -' 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 | (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

n is set

A is set
dom P is Element of K19(n)
K19(n) is set

(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

(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

P is set

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

dom P is set
A is set

rng P is set
dom P is Element of K19(n)
K19(n) is set
i is set
P . i is set

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

() \/ () is finite set

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

dom A is Element of K19(n)
dom L is Element of K19(n)
dom T is Element of K19(n)
i is set

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

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

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

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

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

A is set
dom P is Element of K19(n)
K19(n) is set

max ((T . 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)

i is set

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 set

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

P is set

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

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

P is set

max ((T . P),(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

max ((T . P),(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

n is set

P is set

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 . P) + (L . P) is epsilon-transitive epsilon-connected ordinal natural finite V29() V52() V53() complex ext-real non negative 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

P is set

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

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

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

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

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

n is set

P is set

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

P is set

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

P is set

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

P is set

max ((T . 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),(P . P)) 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

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,A] is V21() set

[i,i] is V21() set
[i,A] is V21() set
[A,i] is V21() set

the carrier of n is non empty non trivial set

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

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 * 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))

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

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

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

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

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