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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
- 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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m + 1 ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= (len x) + (len <*(1. L)*>) ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width (((L,p) * x) * v1) ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len x ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len ((L,p) * (Line (x,v2))) ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Line (x,v2)) ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width x ) } is set
Seg p is Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= p ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= q ) } is set
[:(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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width ((L,p) * x) ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (mlt (((L,p) * (Line (x,v2))),(Col (v1,u9)))) ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (mlt ((Line (x,v2)),(Col (v1,u9)))) ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width v1 ) } is set
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)
{ b1 where b1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width (x * v1) ) } is set
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 (