:: FVSUM_1 semantic presentation

REAL is set

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

K19(REAL) is cup-closed diff-closed preBoolean set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() ext-real non negative V40() finite finite-yielding V47() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

COMPLEX is set

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

K19(NAT) is V12() cup-closed diff-closed preBoolean non finite set

K19(NAT) is V12() cup-closed diff-closed preBoolean non finite set

Fin NAT is non empty cup-closed diff-closed preBoolean 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

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() ext-real non negative V40() finite finite-yielding V47() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered 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

K is non empty add-associative 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

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

K is non empty add-associative 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

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

K is non empty unital commutative right_unital left_unital multLoopStr

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

K is non empty unital commutative right_unital left_unital multLoopStr

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

K is non empty left_zeroed right_zeroed addLoopStr

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

K is non empty left_zeroed right_zeroed 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_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

K is non empty left_zeroed right_zeroed 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

0. K is V63(K) Element of the carrier of K

K is non empty unital commutative right_unital left_unital multLoopStr

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

K is non empty right-distributive left-distributive distributive doubleLoopStr

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

K is non empty 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

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 is non empty addLoopStr

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

K is non empty right-distributive left-distributive distributive doubleLoopStr

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

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

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

K is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed 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) 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

K is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative right_zeroed 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) 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))

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

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

K is non empty 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 Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K

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 .: (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 non empty addLoopStr

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

a1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K

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

a1 is non empty addLoopStr

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

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

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

(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

a2 is non empty addLoopStr

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

p . a1 is set

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

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)

K is non empty addLoopStr

the carrier of K is non empty set

a1 is Element of the carrier of K

<*a1*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on 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

<*a2*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of K

(1,K,<*a1*>,<*a2*>) is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on 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

<*(a1 + a2)*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of K

a1 is non empty addLoopStr

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

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

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

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

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

(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

a1 is non empty left_zeroed Abelian 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 |-> (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

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

(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

K is non empty addLoopStr

the carrier of K is non empty set

a1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence 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

(comp K) * a1 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

a1 is non empty addLoopStr

the carrier of a1 is non empty set

a2 is Element of the carrier of a1

- a2 is Element of the carrier of 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

(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

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

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

a1 is non empty addLoopStr

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

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

(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

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

a2 is non empty addLoopStr

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

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

(comp a2) * b2 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,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)

K is non empty addLoopStr

the carrier of K is non empty set

a1 is Element of the carrier of K

<*a1*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of K

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

(1,K,<*a1*>) is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on 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

(comp K) * <*a1*> is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K

- a1 is Element of the carrier of K

<*(- a1)*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of K

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

<*((comp K) . a1)*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of K

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

a1 is non empty addLoopStr

the carrier of a1 is non empty set

a2 is Element of the carrier of 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

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

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) . a2 is Element of the carrier of a1

K |-> ((comp 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

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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative 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 |-> (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

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

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

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 |-> (the_unity_wrt the addF of 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

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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like Abelian add-associative 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 |-> (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

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

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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative 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 |-> (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

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

(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 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) * a2 is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of 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

(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

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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative 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

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

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

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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative 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

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

(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 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) * a2 is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of 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

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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like add-associative 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

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

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

(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

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

(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

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

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

(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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like Abelian add-associative 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

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

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

(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

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

(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

a1 is non empty left_add-cancelable right_add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like Abelian add-associative 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

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

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

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

(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

K is non empty addLoopStr

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 Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K

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) .: (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

a1 is non empty addLoopStr

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 is Relation-like NAT -defined the carrier of a1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a1

b2 . K is set

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

a1 is non empty addLoopStr

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

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

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

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

a2 is non empty addLoopStr

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

p . K is set

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

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)

K is non empty addLoopStr

the carrier of K is non empty set

a1 is Element of the carrier of K

<*a1*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on 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

<*a2*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of K

(1,K,<*a1*>,<*a2*>) is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on 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))

(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

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