:: FVSUM_1 semantic presentation

REAL is set
NAT is non empty V12() V29() V30() V31() non finite cardinal limit_cardinal Element of K19(REAL)

NAT is non empty V12() V29() V30() V31() non finite cardinal limit_cardinal set

INT is set
1 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite cardinal Element of NAT
2 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite cardinal Element of NAT
3 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite cardinal Element of NAT

Seg 1 is non empty V12() finite 1 -element Element of K19(NAT)
{1} is non empty V12() finite V47() 1 -element set
Seg 2 is non empty finite 2 -element Element of K19(NAT)
{1,2} is non empty finite V47() set
K is non empty Abelian addLoopStr
the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
a1 is Element of the carrier of K
a2 is Element of the carrier of K
the addF of K . (a1,a2) is Element of the carrier of K
a1 + a2 is Element of the carrier of K
the addF of K . (a2,a1) is Element of the carrier of K
the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
a1 is Element of the carrier of K
a2 is Element of the carrier of K
b1 is Element of the carrier of K
the addF of K . (a2,b1) is Element of the carrier of K
the addF of K . (a1,( the addF of K . (a2,b1))) is Element of the carrier of K
a2 + b1 is Element of the carrier of K
a1 + (a2 + b1) is Element of the carrier of K
the addF of K . (a1,(a2 + b1)) is Element of the carrier of K
a1 + a2 is Element of the carrier of K
the addF of K . (a1,a2) is Element of the carrier of K
(a1 + a2) + b1 is Element of the carrier of K
the addF of K . ((a1 + a2),b1) is Element of the carrier of K
the addF of K . (( the addF of K . (a1,a2)),b1) is Element of the carrier of K
K is non empty commutative multMagma
the carrier of K is non empty set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
a1 is Element of the carrier of K
a2 is Element of the carrier of K
the multF of K . (a1,a2) is Element of the carrier of K
a1 * a2 is Element of the carrier of K
a2 * a1 is Element of the carrier of K
the multF of K . (a2,a1) is Element of the carrier of K
K is non empty Abelian addLoopStr
the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
K is non empty commutative multMagma
the carrier of K is non empty set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set

the carrier of K is non empty set
1. K is Element of the carrier of K
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) commutative having_a_unity Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
a2 is Element of the carrier of K
the multF of K . ((1. K),a2) is Element of the carrier of K
(1. K) * a2 is Element of the carrier of K
the multF of K . (a2,(1. K)) is Element of the carrier of K
a2 * (1. K) is Element of the carrier of K

the carrier of K is non empty set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) commutative having_a_unity Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the_unity_wrt the multF of K is Element of the carrier of K
1. K is Element of the carrier of K
a1 is Element of the carrier of K

the carrier of K is non empty set
0. K is V63(K) Element of the carrier of K
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
a1 is Element of the carrier of K
the addF of K . ((0. K),a1) is Element of the carrier of K
(0. K) + a1 is Element of the carrier of K
the addF of K . (a1,(0. K)) is Element of the carrier of K
a1 + (0. K) is Element of the carrier of K

the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the_unity_wrt the addF of K is Element of the carrier of K
0. K is V63(K) Element of the carrier of K
a1 is Element of the carrier of K

the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
0. K is V63(K) Element of the carrier of K

the carrier of K is non empty set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) commutative having_a_unity Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set

the carrier of K is non empty set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
a1 is Element of the carrier of K
a2 is Element of the carrier of K
b1 is Element of the carrier of K
the addF of K . (a2,b1) is Element of the carrier of K
the multF of K . (a1,( the addF of K . (a2,b1))) is Element of the carrier of K
a2 + b1 is Element of the carrier of K
a1 * (a2 + b1) is Element of the carrier of K
the multF of K . (a1,(a2 + b1)) is Element of the carrier of K
a1 * a2 is Element of the carrier of K
the multF of K . (a1,a2) is Element of the carrier of K
a1 * b1 is Element of the carrier of K
the multF of K . (a1,b1) is Element of the carrier of K
(a1 * a2) + (a1 * b1) is Element of the carrier of K
the addF of K . ((a1 * a2),(a1 * b1)) is Element of the carrier of K
the addF of K . (( the multF of K . (a1,a2)),( the multF of K . (a1,b1))) is Element of the carrier of K
the addF of K . (a1,a2) is Element of the carrier of K
the multF of K . (( the addF of K . (a1,a2)),b1) is Element of the carrier of K
a1 + a2 is Element of the carrier of K
(a1 + a2) * b1 is Element of the carrier of K
the multF of K . ((a1 + a2),b1) is Element of the carrier of K
a2 * b1 is Element of the carrier of K
the multF of K . (a2,b1) is Element of the carrier of K
(a1 * b1) + (a2 * b1) is Element of the carrier of K
the addF of K . ((a1 * b1),(a2 * b1)) is Element of the carrier of K
the addF of K . (( the multF of K . (a1,b1)),( the multF of K . (a2,b1))) is Element of the carrier of K
K is non empty multMagma
the carrier of K is non empty set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
a1 is Element of the carrier of K
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
the multF of K [;] (a1,(id the carrier of K)) is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the addF of K * ((id the carrier of K),(comp K)) is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
the carrier of K is non empty set
(K) is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the addF of K * ((id the carrier of K),(comp K)) is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
a1 is Element of the carrier of K
a2 is Element of the carrier of K
(K) . (a1,a2) is Element of the carrier of K
a1 - a2 is Element of the carrier of K
- a2 is Element of the carrier of K
a1 + (- a2) is Element of the carrier of K
the addF of K . (a1,(- a2)) is Element of the carrier of K
(comp K) . a2 is Element of the carrier of K
the addF of K . (a1,((comp K) . a2)) is Element of the carrier of K
K is non empty multMagma
the carrier of K is non empty set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
a2 is Element of the carrier of K
the multF of K [;] (a2,(id the carrier of K)) is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
a1 is Element of the carrier of K
( the multF of K [;] (a2,(id the carrier of K))) . a1 is Element of the carrier of K
a2 * a1 is Element of the carrier of K
the multF of K . (a2,a1) is Element of the carrier of K
(id the carrier of K) . a1 is Element of the carrier of K
the multF of K . (a2,((id the carrier of K) . a1)) is Element of the carrier of K

the carrier of K is non empty set
a1 is Element of the carrier of K
(K,a1) is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
the multF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the multF of K [;] (a1,(id the carrier of K)) is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))

the carrier of K is non empty set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) associative Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
a1 is Element of the carrier of K
(comp K) . a1 is Element of the carrier of K
the addF of K . (a1,((comp K) . a1)) is Element of the carrier of K
- a1 is Element of the carrier of K
a1 + (- a1) is Element of the carrier of K
the addF of K . (a1,(- a1)) is Element of the carrier of K
0. K is V63(K) Element of the carrier of K
the_unity_wrt the addF of K is Element of the carrier of K
the addF of K . (((comp K) . a1),a1) is Element of the carrier of K
(- a1) + a1 is Element of the carrier of K
the addF of K . ((- a1),a1) is Element of the carrier of K

the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) associative Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set

the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) associative Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the_inverseOp_wrt the addF of K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))

the carrier of K is non empty set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) commutative associative Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the_inverseOp_wrt the addF of K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the carrier of K is non empty set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set

the addF of K .: (a1,a2) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the carrier of K is non empty set
p is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

(K,a1,a2) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K .: (a1,a2) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
dom (K,a1,a2) is finite Element of K19(NAT)
b1 is Element of the carrier of K
a1 . p is set
b2 is Element of the carrier of K
a2 . p is set
(K,a1,a2) . p is set
b1 + b2 is Element of the carrier of K
the addF of K . (b1,b2) is Element of the carrier of K
the carrier of a1 is non empty set
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

(a1,a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
Seg K is finite K -element Element of K19(NAT)
a1 is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
the carrier of a2 is non empty set
K -tuples_on the carrier of a2 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a2
b1 is Element of the carrier of a2
b2 is Element of the carrier of a2
b1 + b2 is Element of the carrier of a2
the addF of a2 is Relation-like Function-like total V18(K20( the carrier of a2, the carrier of a2), the carrier of a2) Element of K19(K20(K20( the carrier of a2, the carrier of a2), the carrier of a2))
K20( the carrier of a2, the carrier of a2) is Relation-like set
K20(K20( the carrier of a2, the carrier of a2), the carrier of a2) is Relation-like set
K19(K20(K20( the carrier of a2, the carrier of a2), the carrier of a2)) is cup-closed diff-closed preBoolean set
the addF of a2 . (b1,b2) is Element of the carrier of a2

p . a1 is set

q . a1 is set
(K,a2,p,q) is Relation-like NAT -defined the carrier of a2 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a2
the addF of a2 .: (p,q) is Relation-like NAT -defined the carrier of a2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a2
(K,a2,p,q) . a1 is set
len (K,a2,p,q) is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
Seg (len (K,a2,p,q)) is finite len (K,a2,p,q) -element Element of K19(NAT)
dom (K,a2,p,q) is finite K -element Element of K19(NAT)
the carrier of K is non empty set
a1 is Element of the carrier of K

1 -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
a2 is Element of the carrier of K

the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K .: (<*a1*>,<*a2*>) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
a1 + a2 is Element of the carrier of K
the addF of K . (a1,a2) is Element of the carrier of K

the carrier of a1 is non empty set
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
a2 is Element of the carrier of a1

K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1
b1 is Element of the carrier of a1

(K,a1,(K |-> a2),(K |-> b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: ((K |-> a2),(K |-> b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
a2 + b1 is Element of the carrier of a1
the addF of a1 . (a2,b1) is Element of the carrier of a1

K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
a1 is non empty left_zeroed right_zeroed addLoopStr
the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

(K,a1,a2,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
the_unity_wrt the addF of a1 is Element of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

(K,a1,a2,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) commutative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K |-> (0. a1)),a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K |-> (0. a1)),a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
the carrier of K is non empty set

comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set

K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
the carrier of a1 is non empty set
a2 is Element of the carrier of a1
- a2 is Element of the carrier of a1

(a1,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

dom (a1,b1) is finite Element of K19(NAT)
b1 . K is set
(a1,b1) . K is set
(comp a1) . a2 is Element of the carrier of a1
the carrier of a1 is non empty set
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

(a1,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
a1 is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
Seg a1 is finite a1 -element Element of K19(NAT)
the carrier of a2 is non empty set
a1 -tuples_on the carrier of a2 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a2
b1 is Element of the carrier of a2
- b1 is Element of the carrier of a2

b2 . K is set
(a1,a2,b2) is Relation-like NAT -defined the carrier of a2 -valued Function-like finite a1 -element FinSequence-like FinSubsequence-like Element of a1 -tuples_on the carrier of a2
comp a2 is Relation-like Function-like non empty total V18( the carrier of a2, the carrier of a2) Element of K19(K20( the carrier of a2, the carrier of a2))
K20( the carrier of a2, the carrier of a2) is Relation-like set
K19(K20( the carrier of a2, the carrier of a2)) is cup-closed diff-closed preBoolean set

(a1,a2,b2) . K is set
len (a1,a2,b2) is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
Seg (len (a1,a2,b2)) is finite len (a1,a2,b2) -element Element of K19(NAT)
dom (a1,a2,b2) is finite a1 -element Element of K19(NAT)
the carrier of K is non empty set
a1 is Element of the carrier of K

1 -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set

- a1 is Element of the carrier of K

(comp K) . a1 is Element of the carrier of K

K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
the carrier of a1 is non empty set
a2 is Element of the carrier of a1

K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1
(K,a1,(K |-> a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set
(comp a1) * (K |-> a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
- a2 is Element of the carrier of a1

(comp a1) . a2 is Element of the carrier of a1

K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

(K,a1,a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) associative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
the_inverseOp_wrt the addF of a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
(the_inverseOp_wrt the addF of a1) * a2 is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
the addF of a1 .: (a2,((the_inverseOp_wrt the addF of a1) * a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
the_unity_wrt the addF of a1 is Element of the carrier of a1

K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

(K,a1,a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) commutative associative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,a2),a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,a2),a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

(K,a1,a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) associative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1

the_inverseOp_wrt the addF of a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
the_unity_wrt the addF of a1 is Element of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

(K,a1,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
(comp a1) * (K,a1,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) associative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

(K,a1,(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
(comp a1) * (K,a1,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

(K,a1,a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) associative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1

(K,a1,b2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1

comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set

(K,a1,b1,(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b1,(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,a2,(K,a1,b1,(K,a1,b1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (a2,(K,a1,b1,(K,a1,b1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,b2,b1),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,b2,b1),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,b2,(K,a1,b1,(K,a1,b1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b2,(K,a1,b1,(K,a1,b1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

(K,a1,b2,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b2,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

(K,a1,b1,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) commutative associative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (b1,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1

(K,a1,b2,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b2,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,a2,b2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (a2,b2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT

the carrier of a1 is non empty set
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

(K,a1,a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) commutative associative Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 .: (a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,a2,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set
(comp a1) * (K,a1,a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1

(K,a1,(K,a1,a2),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,a2),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,a2,b1),(K,a1,(K,a1,a2),(K,a1,b1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,a2,b1),(K,a1,(K,a1,a2),(K,a1,b1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,a2,b1),(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,a2,b1),(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,(K,a1,a2,b1),(K,a1,a2)),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,(K,a1,a2,b1),(K,a1,a2)),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,b1,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b1,a2) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,b1,a2),(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,b1,a2),(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,(K,a1,b1,a2),(K,a1,a2)),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,(K,a1,b1,a2),(K,a1,a2)),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (a2,(K,a1,a2)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,b1,(K,a1,a2,(K,a1,a2))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b1,(K,a1,a2,(K,a1,a2))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,b1,(K,a1,a2,(K,a1,a2))),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,b1,(K,a1,a2,(K,a1,a2))),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
0. a1 is V63(a1) Element of the carrier of a1

(K,a1,b1,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b1,(K |-> (0. a1))) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,(K,a1,b1,(K |-> (0. a1))),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: ((K,a1,b1,(K |-> (0. a1))),(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(K,a1,b1,(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of a1
the addF of a1 .: (b1,(K,a1,b1)) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
the carrier of K is non empty set
(K) is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the addF of K * ((id the carrier of K),(comp K)) is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))

(K) .: (a1,a2) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
the carrier of a1 is non empty set
a2 is Element of the carrier of a1
b1 is Element of the carrier of a1
a2 - b1 is Element of the carrier of a1
- b1 is Element of the carrier of a1
a2 + (- b1) is Element of the carrier of a1
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 . (a2,(- b1)) is Element of the carrier of a1

b2 . K is set

(a1,b2,p) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(a1) is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
id the carrier of a1 is Relation-like the carrier of a1 -defined the carrier of a1 -valued Function-like one-to-one non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set
comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
the addF of a1 * ((id the carrier of a1),(comp a1)) is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
(a1) .: (b2,p) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
dom (a1,b2,p) is finite Element of K19(NAT)
p . K is set
(a1,b2,p) . K is set
(a1) . (a2,b1) is Element of the carrier of a1
the carrier of a1 is non empty set
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
K -tuples_on the carrier of a1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a1

(a1,a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
(a1) is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
K20( the carrier of a1, the carrier of a1) is Relation-like set
K20(K20( the carrier of a1, the carrier of a1), the carrier of a1) is Relation-like set
K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1)) is cup-closed diff-closed preBoolean set
the addF of a1 is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
id the carrier of a1 is Relation-like the carrier of a1 -defined the carrier of a1 -valued Function-like one-to-one non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
K19(K20( the carrier of a1, the carrier of a1)) is cup-closed diff-closed preBoolean set
comp a1 is Relation-like Function-like non empty total V18( the carrier of a1, the carrier of a1) Element of K19(K20( the carrier of a1, the carrier of a1))
the addF of a1 * ((id the carrier of a1),(comp a1)) is Relation-like Function-like total V18(K20( the carrier of a1, the carrier of a1), the carrier of a1) Element of K19(K20(K20( the carrier of a1, the carrier of a1), the carrier of a1))
(a1) .: (a2,b1) is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1
K is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
a1 is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
Seg a1 is finite a1 -element Element of K19(NAT)
the carrier of a2 is non empty set
a1 -tuples_on the carrier of a2 is functional non empty FinSequence-membered FinSequenceSet of the carrier of a2
b1 is Element of the carrier of a2
b2 is Element of the carrier of a2
b1 - b2 is Element of the carrier of a2
- b2 is Element of the carrier of a2
b1 + (- b2) is Element of the carrier of a2
the addF of a2 is Relation-like Function-like total V18(K20( the carrier of a2, the carrier of a2), the carrier of a2) Element of K19(K20(K20( the carrier of a2, the carrier of a2), the carrier of a2))
K20( the carrier of a2, the carrier of a2) is Relation-like set
K20(K20( the carrier of a2, the carrier of a2), the carrier of a2) is Relation-like set
K19(K20(K20( the carrier of a2, the carrier of a2), the carrier of a2)) is cup-closed diff-closed preBoolean set
the addF of a2 . (b1,(- b2)) is Element of the carrier of a2

p . K is set

q . K is set
(a1,a2,p,q) is Relation-like NAT -defined the carrier of a2 -valued Function-like finite a1 -element FinSequence-like FinSubsequence-like Element of a1 -tuples_on the carrier of a2
(a2) is Relation-like Function-like total V18(K20( the carrier of a2, the carrier of a2), the carrier of a2) Element of K19(K20(K20( the carrier of a2, the carrier of a2), the carrier of a2))
id the carrier of a2 is Relation-like the carrier of a2 -defined the carrier of a2 -valued Function-like one-to-one non empty total V18( the carrier of a2, the carrier of a2) Element of K19(K20( the carrier of a2, the carrier of a2))
K19(K20( the carrier of a2, the carrier of a2)) is cup-closed diff-closed preBoolean set
comp a2 is Relation-like Function-like non empty total V18( the carrier of a2, the carrier of a2) Element of K19(K20( the carrier of a2, the carrier of a2))
the addF of a2 * ((id the carrier of a2),(comp a2)) is Relation-like Function-like total V18(K20( the carrier of a2, the carrier of a2), the carrier of a2) Element of K19(K20(K20( the carrier of a2, the carrier of a2), the carrier of a2))
(a2) .: (p,q) is Relation-like NAT -defined the carrier of a2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a2
(a1,a2,p,q) . K is set
len (a1,a2,p,q) is V29() V30() V31() V35() V36() ext-real non negative V40() finite cardinal Element of NAT
Seg (len (a1,a2,p,q)) is finite len (a1,a2,p,q) -element Element of K19(NAT)
dom (a1,a2,p,q) is finite a1 -element Element of K19(NAT)
the carrier of K is non empty set
a1 is Element of the carrier of K

1 -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
a2 is Element of the carrier of K

(K) is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
K20( the carrier of K, the carrier of K) is Relation-like set
K20(K20( the carrier of K, the carrier of K), the carrier of K) is Relation-like set
K19(K20(K20( the carrier of K, the carrier of K), the carrier of K)) is cup-closed diff-closed preBoolean set
the addF of K is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
K19(K20( the carrier of K, the carrier of K)) is cup-closed diff-closed preBoolean set
comp K is Relation-like Function-like non empty total V18( the carrier of K, the carrier of K) Element of K19(K20( the carrier of K, the carrier of K))
the addF of K * ((id the carrier of K),(comp K)) is Relation-like Function-like total V18(K20( the carrier of K, the carrier of K), the carrier of K) Element of K19(K20(K20( the carrier of K, the carrier of K), the carrier of K))

a1 - a2 is Element of the carrier of K
- a2 is Element of the carrier of K
a1 + (- a2) is Element of the carrier of K
the addF of K . (a1,(- a2)) is Element of the carrier of K
<*(a1 - a2)