:: POLYNOM8 semantic presentation

REAL is set

NAT is non empty V4() V5() V6() V32() V37() V38() Element of K6(REAL)

K6(REAL) is set

K546() is strict doubleLoopStr

the carrier of K546() is set

COMPLEX is set

NAT is non empty V4() V5() V6() V32() V37() V38() set

K6(NAT) is V32() set

K6(NAT) is V32() set

1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

K7(1,1) is set

K6(K7(1,1)) is set

K7(K7(1,1),1) is set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is set

K7(K7(REAL,REAL),REAL) is set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

K7(2,2) is set

K7(K7(2,2),REAL) is set

K6(K7(K7(2,2),REAL)) is set

RAT is set

INT is set

K6(K7(REAL,REAL)) is set

K364(2) is V190() L18()

the carrier of K364(2) is set

K6( the carrier of K364(2)) is set

{} is empty V4() V5() V6() V8() V9() V10() V11() V12() integer V32() V37() V39( {} ) ext-real non positive non negative set

K7(NAT,REAL) is set

K6(K7(NAT,REAL)) is set

1 -tuples_on NAT is FinSequenceSet of NAT

0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer V32() V37() V39( {} ) ext-real non positive non negative Element of NAT

Seg 1 is Element of K6(NAT)

{ b

- 1 is V11() V12() integer ext-real non positive set

L is V11() V12() integer ext-real set

- L is V11() V12() integer ext-real set

p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

- 0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer V32() V37() V39( {} ) ext-real non positive non negative set

- (- L) is V11() V12() integer ext-real set

L is V11() V12() integer ext-real set

L is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p is non empty non degenerated non trivial unital right_unital well-unital left_unital domRing-like doubleLoopStr

the carrier of p is non empty non trivial set

0. p is V48(p) Element of the carrier of p

q is Element of the carrier of p

q |^ L is Element of the carrier of p

power p is Relation-like K7( the carrier of p,NAT) -defined the carrier of p -valued Function-like V29(K7( the carrier of p,NAT), the carrier of p) Element of K6(K7(K7( the carrier of p,NAT), the carrier of p))

K7( the carrier of p,NAT) is V32() set

K7(K7( the carrier of p,NAT), the carrier of p) is V32() set

K6(K7(K7( the carrier of p,NAT), the carrier of p)) is V32() set

(power p) . (q,L) is set

m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q |^ m is Element of the carrier of p

(power p) . (q,m) is set

(q |^ m) * q is Element of the carrier of p

m + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

q |^ (m + 1) is Element of the carrier of p

(power p) . (q,(m + 1)) is set

q |^ 0 is Element of the carrier of p

(power p) . (q,0) is set

1_ p is Element of the carrier of p

1. p is V48(p) Element of the carrier of p

L is non empty left_add-cancelable right_add-cancelable right_complementable unital associative right-distributive right_unital well-unital left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty set

0. L is V48(L) Element of the carrier of L

p is Element of the carrier of L

q is Element of the carrier of L

p * q is Element of the carrier of L

1. L is Element of the carrier of L

m is Element of the carrier of L

m * p is Element of the carrier of L

(1. L) * q is Element of the carrier of L

m * (p * q) is Element of the carrier of L

L is non empty left_add-cancelable right_add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty set

0. L is V48(L) Element of the carrier of L

p is Element of the carrier of L

q is Element of the carrier of L

p * q is Element of the carrier of L

(p * q) " is Element of the carrier of L

p " is Element of the carrier of L

q " is Element of the carrier of L

(p ") * (q ") is Element of the carrier of L

((p ") * (q ")) * (p * q) is Element of the carrier of L

((p ") * (q ")) * q is Element of the carrier of L

(((p ") * (q ")) * q) * p is Element of the carrier of L

(q ") * q is Element of the carrier of L

(p ") * ((q ") * q) is Element of the carrier of L

((p ") * ((q ") * q)) * p is Element of the carrier of L

1. L is Element of the carrier of L

(p ") * (1. L) is Element of the carrier of L

((p ") * (1. L)) * p is Element of the carrier of L

(p ") * p is Element of the carrier of L

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

0. L is V48(L) Element of the carrier of L

p is Element of the carrier of L

q is Element of the carrier of L

q * p is Element of the carrier of L

(q * p) / p is Element of the carrier of L

p " is Element of the carrier of L

(q * p) * (p ") is Element of the carrier of L

p * (p ") is Element of the carrier of L

q * (p * (p ")) is Element of the carrier of L

1. L is Element of the carrier of L

q * (1. L) is Element of the carrier of L

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

the carrier of L is non empty set

1. L is Element of the carrier of L

p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p * (1. L) is Element of the carrier of L

K572(L) is Relation-like K7(NAT, the carrier of L) -defined the carrier of L -valued Function-like V29(K7(NAT, the carrier of L), the carrier of L) Element of K6(K7(K7(NAT, the carrier of L), the carrier of L))

K7(NAT, the carrier of L) is V32() set

K7(K7(NAT, the carrier of L), the carrier of L) is V32() set

K6(K7(K7(NAT, the carrier of L), the carrier of L)) is V32() set

K572(L) . (p,(1. L)) is Element of the carrier of L

q is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Sum q is Element of the carrier of L

m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

m * (1. L) is Element of the carrier of L

K572(L) . (m,(1. L)) is Element of the carrier of L

m + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

(m + 1) * (1. L) is Element of the carrier of L

K572(L) . ((m + 1),(1. L)) is Element of the carrier of L

Seg m is Element of K6(NAT)

{ b

x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

dom x is Element of K6(NAT)

x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

dom x is Element of K6(NAT)

x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

dom x is Element of K6(NAT)

len x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

x /. v1 is Element of the carrier of L

x . v1 is set

v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

x /. v1 is Element of the carrier of L

<*(1. L)*> is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

[1,(1. L)] is V26() set

{[1,(1. L)]} is non empty trivial V39(1) set

dom <*(1. L)*> is Element of K6(NAT)

len <*(1. L)*> is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

v1 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Sum v1 is Element of the carrier of L

dom v1 is Element of K6(NAT)

Seg (m + 1) is Element of K6(NAT)

{ b

x ^ <*(1. L)*> is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

v1 . v2 is set

(x ^ <*(1. L)*>) . v2 is set

x . v2 is set

x /. v2 is Element of the carrier of L

v1 /. v2 is Element of the carrier of L

v2 - v2 is V11() V12() integer ext-real set

(m + 1) - v2 is V11() V12() integer ext-real set

((m + 1) - v2) + 1 is V11() V12() integer ext-real set

u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(v2 - v2) + 1 is V11() V12() integer ext-real set

v2 + m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

m + 0 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(m + 1) - m is V11() V12() integer ext-real set

(v2 + m) - m is V11() V12() integer ext-real set

(len x) + u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(x ^ <*(1. L)*>) . ((len x) + u9) is set

<*(1. L)*> . 1 is set

v1 /. v2 is Element of the carrier of L

dom (x ^ <*(1. L)*>) is Element of K6(NAT)

(len x) + (len <*(1. L)*>) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg ((len x) + (len <*(1. L)*>)) is Element of K6(NAT)

{ b

Sum x is Element of the carrier of L

(Sum x) + (1. L) is Element of the carrier of L

(m * (1. L)) + (1. L) is Element of the carrier of L

1 * (1. L) is Element of the carrier of L

K572(L) . (1,(1. L)) is Element of the carrier of L

(m * (1. L)) + (1 * (1. L)) is Element of the carrier of L

x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Sum x is Element of the carrier of L

0 * (1. L) is Element of the carrier of L

K572(L) . (0,(1. L)) is Element of the carrier of L

m is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Sum m is Element of the carrier of L

<*> the carrier of L is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

0 -tuples_on the carrier of L is FinSequenceSet of the carrier of L

Sum (<*> the carrier of L) is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

m is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Sum m is Element of the carrier of L

L is non empty left_add-cancelable right_add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty set

1. L is Element of the carrier of L

p is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Sum p is Element of the carrier of L

q is Element of the carrier of L

q |^ (len p) is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . (q,(len p)) is set

(1. L) - (q |^ (len p)) is Element of the carrier of L

- (q |^ (len p)) is Element of the carrier of L

(1. L) + (- (q |^ (len p))) is Element of the carrier of L

(1. L) - q is Element of the carrier of L

- q is Element of the carrier of L

(1. L) + (- q) is Element of the carrier of L

((1. L) - (q |^ (len p))) / ((1. L) - q) is Element of the carrier of L

((1. L) - q) " is Element of the carrier of L

((1. L) - (q |^ (len p))) * (((1. L) - q) ") is Element of the carrier of L

m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

m + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

Seg m is Element of K6(NAT)

{ b

x | (Seg m) is Relation-like NAT -defined the carrier of L -valued Function-like Element of K6(K7(NAT, the carrier of L))

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

len x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

dom x is Element of K6(NAT)

x /. (len x) is Element of the carrier of L

x . (len x) is set

v2 is Relation-like Function-like FinSequence-like set

len v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

u9 is set

rng v2 is set

dom v2 is Element of K6(NAT)

u is set

v2 . u is set

k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

x . u is set

x /. u is Element of the carrier of L

u9 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(len u9) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

u is Element of the carrier of L

(1. L) - u is Element of the carrier of L

- u is Element of the carrier of L

(1. L) + (- u) is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

((1. L) - u) + u is Element of the carrier of L

(- u) + u is Element of the carrier of L

(1. L) + ((- u) + u) is Element of the carrier of L

(1. L) + (0. L) is Element of the carrier of L

1 - 1 is V11() V12() integer ext-real set

(len x) - 1 is V11() V12() integer ext-real set

(len x) -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

((len u9) + 1) - 1 is V11() V12() integer ext-real set

k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

dom u9 is Element of K6(NAT)

u9 . k is set

x . k is set

k -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

u |^ (k -' 1) is Element of the carrier of L

(power L) . (u,(k -' 1)) is set

x | (dom u9) is Relation-like NAT -defined the carrier of L -valued Function-like Element of K6(K7(NAT, the carrier of L))

Sum x is Element of the carrier of L

Sum u9 is Element of the carrier of L

(Sum u9) + (x /. (len x)) is Element of the carrier of L

u |^ (len u9) is Element of the carrier of L

(power L) . (u,(len u9)) is set

(1. L) - (u |^ (len u9)) is Element of the carrier of L

- (u |^ (len u9)) is Element of the carrier of L

(1. L) + (- (u |^ (len u9))) is Element of the carrier of L

((1. L) - (u |^ (len u9))) / ((1. L) - u) is Element of the carrier of L

((1. L) - u) " is Element of the carrier of L

((1. L) - (u |^ (len u9))) * (((1. L) - u) ") is Element of the carrier of L

(((1. L) - (u |^ (len u9))) / ((1. L) - u)) + (x /. (len x)) is Element of the carrier of L

(((1. L) - (u |^ (len u9))) / ((1. L) - u)) + (u |^ (len u9)) is Element of the carrier of L

(u |^ (len u9)) * ((1. L) - u) is Element of the carrier of L

((u |^ (len u9)) * ((1. L) - u)) / ((1. L) - u) is Element of the carrier of L

((u |^ (len u9)) * ((1. L) - u)) * (((1. L) - u) ") is Element of the carrier of L

(((1. L) - (u |^ (len u9))) / ((1. L) - u)) + (((u |^ (len u9)) * ((1. L) - u)) / ((1. L) - u)) is Element of the carrier of L

((1. L) - (u |^ (len u9))) + ((u |^ (len u9)) * ((1. L) - u)) is Element of the carrier of L

(((1. L) - (u |^ (len u9))) + ((u |^ (len u9)) * ((1. L) - u))) / ((1. L) - u) is Element of the carrier of L

(((1. L) - (u |^ (len u9))) + ((u |^ (len u9)) * ((1. L) - u))) * (((1. L) - u) ") is Element of the carrier of L

(u |^ (len u9)) * (1. L) is Element of the carrier of L

(u |^ (len u9)) * (- u) is Element of the carrier of L

((u |^ (len u9)) * (1. L)) + ((u |^ (len u9)) * (- u)) is Element of the carrier of L

((1. L) - (u |^ (len u9))) + (((u |^ (len u9)) * (1. L)) + ((u |^ (len u9)) * (- u))) is Element of the carrier of L

(((1. L) - (u |^ (len u9))) + (((u |^ (len u9)) * (1. L)) + ((u |^ (len u9)) * (- u)))) / ((1. L) - u) is Element of the carrier of L

(((1. L) - (u |^ (len u9))) + (((u |^ (len u9)) * (1. L)) + ((u |^ (len u9)) * (- u)))) * (((1. L) - u) ") is Element of the carrier of L

(u |^ (len u9)) + ((u |^ (len u9)) * (- u)) is Element of the carrier of L

((1. L) - (u |^ (len u9))) + ((u |^ (len u9)) + ((u |^ (len u9)) * (- u))) is Element of the carrier of L

(((1. L) - (u |^ (len u9))) + ((u |^ (len u9)) + ((u |^ (len u9)) * (- u)))) / ((1. L) - u) is Element of the carrier of L

(((1. L) - (u |^ (len u9))) + ((u |^ (len u9)) + ((u |^ (len u9)) * (- u)))) * (((1. L) - u) ") is Element of the carrier of L

(- (u |^ (len u9))) + ((u |^ (len u9)) + ((u |^ (len u9)) * (- u))) is Element of the carrier of L

(1. L) + ((- (u |^ (len u9))) + ((u |^ (len u9)) + ((u |^ (len u9)) * (- u)))) is Element of the carrier of L

((1. L) + ((- (u |^ (len u9))) + ((u |^ (len u9)) + ((u |^ (len u9)) * (- u))))) / ((1. L) - u) is Element of the carrier of L

((1. L) + ((- (u |^ (len u9))) + ((u |^ (len u9)) + ((u |^ (len u9)) * (- u))))) * (((1. L) - u) ") is Element of the carrier of L

(- (u |^ (len u9))) + (u |^ (len u9)) is Element of the carrier of L

((- (u |^ (len u9))) + (u |^ (len u9))) + ((u |^ (len u9)) * (- u)) is Element of the carrier of L

(1. L) + (((- (u |^ (len u9))) + (u |^ (len u9))) + ((u |^ (len u9)) * (- u))) is Element of the carrier of L

((1. L) + (((- (u |^ (len u9))) + (u |^ (len u9))) + ((u |^ (len u9)) * (- u)))) / ((1. L) - u) is Element of the carrier of L

((1. L) + (((- (u |^ (len u9))) + (u |^ (len u9))) + ((u |^ (len u9)) * (- u)))) * (((1. L) - u) ") is Element of the carrier of L

(0. L) + ((u |^ (len u9)) * (- u)) is Element of the carrier of L

(1. L) + ((0. L) + ((u |^ (len u9)) * (- u))) is Element of the carrier of L

((1. L) + ((0. L) + ((u |^ (len u9)) * (- u)))) / ((1. L) - u) is Element of the carrier of L

((1. L) + ((0. L) + ((u |^ (len u9)) * (- u)))) * (((1. L) - u) ") is Element of the carrier of L

(1. L) + ((u |^ (len u9)) * (- u)) is Element of the carrier of L

((1. L) + ((u |^ (len u9)) * (- u))) / ((1. L) - u) is Element of the carrier of L

((1. L) + ((u |^ (len u9)) * (- u))) * (((1. L) - u) ") is Element of the carrier of L

(u |^ (len u9)) * u is Element of the carrier of L

- ((u |^ (len u9)) * u) is Element of the carrier of L

(1. L) + (- ((u |^ (len u9)) * u)) is Element of the carrier of L

((1. L) + (- ((u |^ (len u9)) * u))) / ((1. L) - u) is Element of the carrier of L

((1. L) + (- ((u |^ (len u9)) * u))) * (((1. L) - u) ") is Element of the carrier of L

u |^ (len x) is Element of the carrier of L

(power L) . (u,(len x)) is set

(1. L) - (u |^ (len x)) is Element of the carrier of L

- (u |^ (len x)) is Element of the carrier of L

(1. L) + (- (u |^ (len x))) is Element of the carrier of L

((1. L) - (u |^ (len x))) / ((1. L) - u) is Element of the carrier of L

((1. L) - (u |^ (len x))) * (((1. L) - u) ") is Element of the carrier of L

x is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

v1 is Element of the carrier of L

Sum x is Element of the carrier of L

v1 |^ (len x) is Element of the carrier of L

(power L) . (v1,(len x)) is set

(1. L) - (v1 |^ (len x)) is Element of the carrier of L

- (v1 |^ (len x)) is Element of the carrier of L

(1. L) + (- (v1 |^ (len x))) is Element of the carrier of L

(1. L) - v1 is Element of the carrier of L

- v1 is Element of the carrier of L

(1. L) + (- v1) is Element of the carrier of L

((1. L) - (v1 |^ (len x))) / ((1. L) - v1) is Element of the carrier of L

((1. L) - v1) " is Element of the carrier of L

((1. L) - (v1 |^ (len x))) * (((1. L) - v1) ") is Element of the carrier of L

m is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

<*> the carrier of L is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

x is Element of the carrier of L

x |^ 0 is Element of the carrier of L

(power L) . (x,0) is set

(1. L) - (x |^ 0) is Element of the carrier of L

- (x |^ 0) is Element of the carrier of L

(1. L) + (- (x |^ 0)) is Element of the carrier of L

(1. L) - x is Element of the carrier of L

- x is Element of the carrier of L

(1. L) + (- x) is Element of the carrier of L

((1. L) - (x |^ 0)) / ((1. L) - x) is Element of the carrier of L

((1. L) - x) " is Element of the carrier of L

((1. L) - (x |^ 0)) * (((1. L) - x) ") is Element of the carrier of L

1_ L is Element of the carrier of L

(1. L) - (1_ L) is Element of the carrier of L

- (1_ L) is Element of the carrier of L

(1. L) + (- (1_ L)) is Element of the carrier of L

((1. L) - (1_ L)) / ((1. L) - x) is Element of the carrier of L

((1. L) - (1_ L)) * (((1. L) - x) ") is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

(0. L) / ((1. L) - x) is Element of the carrier of L

(0. L) * (((1. L) - x) ") is Element of the carrier of L

Sum m is Element of the carrier of L

m is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

x is Element of the carrier of L

Sum m is Element of the carrier of L

x |^ (len m) is Element of the carrier of L

(power L) . (x,(len m)) is set

(1. L) - (x |^ (len m)) is Element of the carrier of L

- (x |^ (len m)) is Element of the carrier of L

(1. L) + (- (x |^ (len m))) is Element of the carrier of L

(1. L) - x is Element of the carrier of L

- x is Element of the carrier of L

(1. L) + (- x) is Element of the carrier of L

((1. L) - (x |^ (len m))) / ((1. L) - x) is Element of the carrier of L

((1. L) - x) " is Element of the carrier of L

((1. L) - (x |^ (len m))) * (((1. L) - x) ") is Element of the carrier of L

L is non empty unital right_unital well-unital left_unital doubleLoopStr

1. L is Element of the carrier of L

the carrier of L is non empty set

p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p * (1. L) is Element of the carrier of L

K572(L) is Relation-like K7(NAT, the carrier of L) -defined the carrier of L -valued Function-like V29(K7(NAT, the carrier of L), the carrier of L) Element of K6(K7(K7(NAT, the carrier of L), the carrier of L))

K7(NAT, the carrier of L) is V32() set

K7(K7(NAT, the carrier of L), the carrier of L) is V32() set

K6(K7(K7(NAT, the carrier of L), the carrier of L)) is V32() set

K572(L) . (p,(1. L)) is Element of the carrier of L

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty non trivial set

the carrier of L * is FinSequenceSet of the carrier of L

p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(L,p) is Element of the carrier of L

1. L is V48(L) Element of the carrier of L

p * (1. L) is Element of the carrier of L

K572(L) is Relation-like K7(NAT, the carrier of L) -defined the carrier of L -valued Function-like V29(K7(NAT, the carrier of L), the carrier of L) Element of K6(K7(K7(NAT, the carrier of L), the carrier of L))

K7(NAT, the carrier of L) is V32() set

K7(K7(NAT, the carrier of L), the carrier of L) is V32() set

K6(K7(K7(NAT, the carrier of L), the carrier of L)) is V32() set

K572(L) . (p,(1. L)) is Element of the carrier of L

x is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,q, the carrier of L

(L,p) * x is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *

v1 is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of q,m, the carrier of L

((L,p) * x) * v1 is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *

x * v1 is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *

(L,p) * (x * v1) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *

width x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

width ((L,p) * x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Indices (((L,p) * x) * v1) is set

dom (((L,p) * x) * v1) is Element of K6(NAT)

width (((L,p) * x) * v1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (width (((L,p) * x) * v1)) is Element of K6(NAT)

{ b

K7((dom (((L,p) * x) * v1)),(Seg (width (((L,p) * x) * v1)))) is set

v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

[v2,u9] is V26() set

(((L,p) * x) * v1) * (v2,u9) is Element of the carrier of L

((L,p) * (x * v1)) * (v2,u9) is Element of the carrier of L

len x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len (x * v1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len (((L,p) * x) * v1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len ((L,p) * x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (len x) is Element of K6(NAT)

{ b

dom (x * v1) is Element of K6(NAT)

Line (x,v2) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (width x) -tuples_on the carrier of L

(width x) -tuples_on the carrier of L is FinSequenceSet of the carrier of L

(L,p) * (Line (x,v2)) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (width x) -tuples_on the carrier of L

len ((L,p) * (Line (x,v2))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (len ((L,p) * (Line (x,v2)))) is Element of K6(NAT)

{ b

dom ((L,p) * (Line (x,v2))) is Element of K6(NAT)

dom (Line (x,v2)) is Element of K6(NAT)

len (Line (x,v2)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (len (Line (x,v2))) is Element of K6(NAT)

{ b

Col (v1,u9) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (len v1) -tuples_on the carrier of L

(len v1) -tuples_on the carrier of L is FinSequenceSet of the carrier of L

len (Col (v1,u9)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Line (((L,p) * x),v2) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (width ((L,p) * x)) -tuples_on the carrier of L

(width ((L,p) * x)) -tuples_on the carrier of L is FinSequenceSet of the carrier of L

(Line (((L,p) * x),v2)) "*" (Col (v1,u9)) is Element of the carrier of L

mlt ((Line (((L,p) * x),v2)),(Col (v1,u9))) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

Sum (mlt ((Line (((L,p) * x),v2)),(Col (v1,u9)))) is Element of the carrier of L

len (Line (((L,p) * x),v2)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

dom (Line (((L,p) * x),v2)) is Element of K6(NAT)

Seg (width x) is Element of K6(NAT)

{ b

Seg p is Element of K6(NAT)

{ b

Indices x is set

dom x is Element of K6(NAT)

K7((dom x),(Seg (width x))) is set

Seg q is Element of K6(NAT)

{ b

[:(Seg p),(Seg q):] is Relation-like NAT -defined NAT -valued Element of K6(K7(NAT,NAT))

K7(NAT,NAT) is V32() set

K6(K7(NAT,NAT)) is V32() set

u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

(Line (((L,p) * x),v2)) . u is set

((L,p) * (Line (x,v2))) . u is set

(Line (x,v2)) . u is set

(Line (x,v2)) /. u is Element of the carrier of L

k is Element of the carrier of L

x * (v2,u) is Element of the carrier of L

[v2,u] is V26() set

(L,p) * k is Element of the carrier of L

((L,p) * x) * (v2,u) is Element of the carrier of L

Seg (width ((L,p) * x)) is Element of K6(NAT)

{ b

mlt (((L,p) * (Line (x,v2))),(Col (v1,u9))) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len (mlt (((L,p) * (Line (x,v2))),(Col (v1,u9)))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (len (mlt (((L,p) * (Line (x,v2))),(Col (v1,u9))))) is Element of K6(NAT)

{ b

dom (mlt (((L,p) * (Line (x,v2))),(Col (v1,u9)))) is Element of K6(NAT)

mlt ((Line (x,v2)),(Col (v1,u9))) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

len (mlt ((Line (x,v2)),(Col (v1,u9)))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (len (mlt ((Line (x,v2)),(Col (v1,u9))))) is Element of K6(NAT)

{ b

dom (mlt ((Line (x,v2)),(Col (v1,u9)))) is Element of K6(NAT)

(L,p) * (mlt ((Line (x,v2)),(Col (v1,u9)))) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L

dom ((L,p) * (mlt ((Line (x,v2)),(Col (v1,u9))))) is Element of K6(NAT)

u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

(mlt (((L,p) * (Line (x,v2))),(Col (v1,u9)))) . u is set

((L,p) * (mlt ((Line (x,v2)),(Col (v1,u9))))) . u is set

dom v1 is Element of K6(NAT)

(Col (v1,u9)) . u is set

v1 * (u,u9) is Element of the carrier of L

(Line (x,v2)) . u is set

x * (v2,u) is Element of the carrier of L

(mlt ((Line (x,v2)),(Col (v1,u9)))) . u is set

k is Element of the carrier of L

l is Element of the carrier of L

k * l is Element of the carrier of L

lengthG is Element of the carrier of L

(L,p) * lengthG is Element of the carrier of L

((L,p) * (Line (x,v2))) . u is set

(L,p) * l is Element of the carrier of L

b is Element of the carrier of L

b * k is Element of the carrier of L

((L,p) * l) * k is Element of the carrier of L

l * k is Element of the carrier of L

(L,p) * (l * k) is Element of the carrier of L

width v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (width v1) is Element of K6(NAT)

{ b

width (x * v1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

Seg (width (x * v1)) is Element of K6(NAT)

{ b

Indices (x * v1) is set

K7((dom (x * v1)),(Seg (width (x * v1)))) is set

(x * v1) * (v2,u9) is Element of the carrier of L

(L,p) * ((x * v1) * (v2,u9)) is Element of the carrier of L

(Line (x,v2)) "*" (Col (v1,u9)) is Element of the carrier of L

(L,p) * ((Line (x,v2)) "*" (Col (v1,u9))) is Element of the carrier of L

Sum (mlt ((Line (x,v2)),(Col (v1,u9)))) is Element of the carrier of L

(L,p) * (Sum (mlt ((Line (x,v2)),(Col (v1,u9))))) is Element of the carrier of L

len ((L,p) * (x * v1)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len (x * v1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

width ((L,p) * (x * v1)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

width (x * v1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

width v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len (((L,p) * x) * v1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len ((L,p) * x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

L is non empty ZeroStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

0. L is V48(L) Element of the carrier of L

p is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p . q is Element of the carrier of L

q + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

L is non empty ZeroStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

0. L is V48(L) Element of the carrier of L

p is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(len p) - 1 is V11() V12() integer ext-real set

p . ((len p) - 1) is set

0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

1 - 1 is V11() V12() integer ext-real set

q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

p . m is Element of the carrier of L

q + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

p . m is Element of the carrier of L

(len p) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

((len p) + 1) - 1 is V11() V12() integer ext-real set

L is non empty left_add-cancelable right_add-cancelable right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

p is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p *' q is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len (p *' q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(len p) + (len q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

((len p) + (len q)) - 1 is V11() V12() integer ext-real set

((len p) + (len q)) - 0 is V11() V12() integer ext-real non negative set

(len q) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

1 - 1 is V11() V12() integer ext-real set

(len q) - 1 is V11() V12() integer ext-real set

q . ((len q) - 1) is set

0. L is V48(L) Element of the carrier of L

(len q) -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q . ((len q) -' 1) is Element of the carrier of L

(len p) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

(len p) - 1 is V11() V12() integer ext-real set

p . ((len p) - 1) is set

(len p) -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p . ((len p) -' 1) is Element of the carrier of L

(p . ((len p) -' 1)) * (q . ((len q) -' 1)) is Element of the carrier of L

L is non empty associative doubleLoopStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

q is Element of the carrier of L

p is Element of the carrier of L

p * q is Element of the carrier of L

m is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

q * m is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

p * (q * m) is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

(p * q) * m is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(p * (q * m)) . x is Element of the carrier of L

(q * m) . x is Element of the carrier of L

p * ((q * m) . x) is Element of the carrier of L

m . x is Element of the carrier of L

q * (m . x) is Element of the carrier of L

p * (q * (m . x)) is Element of the carrier of L

(p * q) * (m . x) is Element of the carrier of L

((p * q) * m) . x is Element of the carrier of L

L is non empty doubleLoopStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

p is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

q is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

m is set

p /. m is Element of the carrier of L

q /. m is Element of the carrier of L

(p /. m) * (q /. m) is Element of the carrier of L

m is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

x is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

dom q is set

q /. v1 is Element of the carrier of L

q . v1 is Element of the carrier of L

dom p is set

p /. v1 is Element of the carrier of L

p . v1 is Element of the carrier of L

x . v1 is Element of the carrier of L

(p . v1) * (q . v1) is Element of the carrier of L

v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

x . v1 is Element of the carrier of L

p . v1 is Element of the carrier of L

q . v1 is Element of the carrier of L

(p . v1) * (q . v1) is Element of the carrier of L

m is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

x is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

v1 is set

dom m is set

m . v1 is set

v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p . v2 is Element of the carrier of L

q . v2 is Element of the carrier of L

(p . v2) * (q . v2) is Element of the carrier of L

x . v1 is set

dom x is set

L is non empty left_add-cancelable right_add-cancelable right_complementable left-distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

p is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

q is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

(L,p,q) is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) Element of K6(K7(NAT, the carrier of L))

0. L is V48(L) Element of the carrier of L

len p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(len p) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

p . x is Element of the carrier of L

q . x is Element of the carrier of L

(p . x) * (q . x) is Element of the carrier of L

(L,p,q) . x is Element of the carrier of L

x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

(L,p,q) . x is Element of the carrier of L

x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

L is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

p is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

q is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

(L,p,q) is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len (L,p,q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

len q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

min ((len p),(len q)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set

p . v2 is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

q . v2 is Element of the carrier of L

(p . v2) * (q . v2) is Element of the carrier of L

(L,p,q) . v2 is Element of the carrier of L

q . v2 is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

p . v2 is Element of the carrier of L

(p . v2) * (q . v2) is Element of the carrier of L

(L,p,q) . v2 is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

0. L is V48(L) Element of the carrier of L

L is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty set

K7(NAT, the carrier of L) is V32() set

K6(K7(NAT, the carrier of L)) is V32() set

p is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(L,p,q) is Relation-like NAT -defined the carrier of L -valued Function-like V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))

len (L,p,q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

1 - 1 is V11() V12() integer ext-real set

(len p) - 1 is V11() V12() integer ext-real set

x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

x + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

(len p) + 0 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

p . x is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

q . x is Element of the carrier of L

(p . x) * (q . x) is Element of the carrier of L

(L,p,q) . x is Element of the carrier of L

min ((len p),(len q)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

q is V11() V12() integer ext-real set

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

p is Element of the carrier of L

(power L) . (p,q) is set

abs q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(power L) . (p,(abs q)) is Element of the carrier of L

((power L) . (p,(abs q))) " is Element of the carrier of L

m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(power L) . (p,m) is Element of the carrier of L

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

1. L is Element of the carrier of L

p is Element of the carrier of L

(L,p,0) is Element of the carrier of L

p |^ 0 is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . (p,0) is set

1_ L is Element of the carrier of L

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

p is Element of the carrier of L

q is V11() V12() integer ext-real set

(L,p,q) is Element of the carrier of L

abs q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(L,p,(abs q)) is Element of the carrier of L

(L,p,(abs q)) " is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . (p,(abs q)) is Element of the carrier of L

L is non empty non degenerated non trivial almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty non trivial set

p is V11() V12() integer ext-real set

abs p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q is Element of the carrier of L

(L,q,p) is Element of the carrier of L

(L,q,(abs p)) is Element of the carrier of L

(L,q,(abs p)) " is Element of the carrier of L

1. L is V48(L) Element of the carrier of L

0. L is V48(L) Element of the carrier of L

(1. L) " is Element of the carrier of L

(1. L) * ((1. L) ") is Element of the carrier of L

1_ L is Element of the carrier of L

(1_ L) " is Element of the carrier of L

q |^ 0 is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . (q,0) is set

(q |^ 0) " is Element of the carrier of L

q |^ (abs p) is Element of the carrier of L

(power L) . (q,(abs p)) is set

(q |^ (abs p)) " is Element of the carrier of L

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

p is Element of the carrier of L

(L,p,1) is Element of the carrier of L

p |^ 1 is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . (p,1) is set

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

p is Element of the carrier of L

(L,p,(- 1)) is Element of the carrier of L

p " is Element of the carrier of L

abs (- 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

- (- 1) is V11() V12() integer ext-real non negative set

(L,p,1) is Element of the carrier of L

(L,p,1) " is Element of the carrier of L

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

1. L is Element of the carrier of L

the carrier of L is non empty set

p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(L,(1. L),p) is Element of the carrier of L

q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(L,(1. L),q) is Element of the carrier of L

q + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

(L,(1. L),(q + 1)) is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . ((1. L),(q + 1)) is Element of the carrier of L

(power L) . ((1. L),q) is Element of the carrier of L

((power L) . ((1. L),q)) * (1. L) is Element of the carrier of L

(1. L) * (1. L) is Element of the carrier of L

1_ L is Element of the carrier of L

(L,(1_ L),0) is Element of the carrier of L

(power L) . ((1. L),0) is Element of the carrier of L

(L,(1. L),0) is Element of the carrier of L

L is non empty non degenerated non trivial almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

1. L is V48(L) Element of the carrier of L

the carrier of L is non empty non trivial set

p is V11() V12() integer ext-real set

(L,(1. L),p) is Element of the carrier of L

0. L is V48(L) Element of the carrier of L

(1. L) * (1. L) is Element of the carrier of L

abs p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(L,(1. L),(abs p)) is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . ((1. L),(abs p)) is Element of the carrier of L

((power L) . ((1. L),(abs p))) " is Element of the carrier of L

(1. L) " is Element of the carrier of L

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

p is Element of the carrier of L

q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

(L,p,(q + 1)) is Element of the carrier of L

(L,p,q) is Element of the carrier of L

(L,p,q) * p is Element of the carrier of L

p * (L,p,q) is Element of the carrier of L

p |^ (q + 1) is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . (p,(q + 1)) is set

p |^ q is Element of the carrier of L

(power L) . (p,q) is set

(p |^ q) * p is Element of the carrier of L

L is non empty unital right_unital well-unital left_unital doubleLoopStr

1. L is Element of the carrier of L

the carrier of L is non empty set

p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(1. L) |^ p is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . ((1. L),p) is set

1_ L is Element of the carrier of L

q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(1. L) |^ q is Element of the carrier of L

(power L) . ((1. L),q) is set

q + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT

(1. L) |^ (q + 1) is Element of the carrier of L

(power L) . ((1. L),(q + 1)) is set

((1. L) |^ q) * (1. L) is Element of the carrier of L

(1. L) |^ 0 is Element of the carrier of L

(power L) . ((1. L),0) is set

L is non empty almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of L is non empty set

0. L is V48(L) Element of the carrier of L

1. L is Element of the carrier of L

p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

q is Element of the carrier of L

q |^ p is Element of the carrier of L

power L is Relation-like K7( the carrier of L,NAT) -defined the carrier of L -valued Function-like V29(K7( the carrier of L,NAT), the carrier of L) Element of K6(K7(K7( the carrier of L,NAT), the carrier of L))

K7( the carrier of L,NAT) is V32() set

K7(K7( the carrier of L,NAT), the carrier of L) is V32() set

K6(K7(K7( the carrier of L,NAT), the carrier of L)) is V32() set

(power L) . (q,p) is set

q " is Element of the carrier of L

(q ") |^ p is Element of the carrier of L

(power L) . ((q "),p) is set

(q |^ p) * ((q ") |^ p) is Element of the carrier of L

q * (q ") is Element of the carrier of L

(q * (q ")) |^ p is Element of the carrier of L

(power L) . ((q * (q ")),p) is set

(1. L) |^ p is Element of the carrier of L

(power L) . ((1. L),p) is set

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non empty non trivial set

0. L is V48(L) Element of the carrier of L

p is V11() V12() integer ext-real set

- p is V11() V12() integer ext-real set

q is Element of the carrier of L

(L,q,p) is Element of the carrier of L

(L,q,p) " is Element of the carrier of L

(L,q,(- p)) is Element of the carrier of L

1. L is V48(L) Element of the carrier of L

- 0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer V32() V37() V39( {} ) ext-real non positive non negative set

abs (- p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT

(L,q,(abs (