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 (- p))) is Element of the carrier of L
(L,q,(abs (- p))) " is Element of the carrier of L
- (- p) is V11() V12() integer ext-real set
(L,q,(- (- p))) is Element of the carrier of L
(L,q,(- (- p))) " 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
- 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 p)) is Element of the carrier of L
q |^ (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) . (q,(abs p)) is set
(L,q,(abs p)) " 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
0. L is V48(L) Element of the carrier of L
p is V11() V12() integer ext-real set
p + 1 is V11() V12() integer ext-real set
q is Element of the carrier of L
(L,q,(p + 1)) is Element of the carrier of L
(L,q,p) is Element of the carrier of L
(L,q,1) is Element of the carrier of L
(L,q,p) * (L,q,1) is Element of the carrier of L
(L,q,(- 1)) 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
q |^ (abs (- 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) . (q,(abs (- 1))) is set
(q |^ (abs (- 1))) " is Element of the carrier of L
- p is V11() V12() integer ext-real set
(L,q,(- p)) 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
q |^ m is Element of the carrier of L
(power L) . (q,m) is set
abs (- p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
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
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 L
(power L) . (q,m) is set
abs (p + 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q |^ (abs (p + 1)) is Element of the carrier of L
(power L) . (q,(abs (p + 1))) is set
(q |^ (abs (p + 1))) " 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 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
abs (p + 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
abs p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,q,(abs p)) is Element of the carrier of L
q |^ (abs p) is Element of the carrier of L
(power L) . (q,(abs p)) is set
(L,q,(abs (p + 1))) is Element of the carrier of L
q |^ (abs (p + 1)) is Element of the carrier of L
(power L) . (q,(abs (p + 1))) is set
(L,q,(- 1)) * (L,q,(- p)) is Element of the carrier of L
(L,q,(p + 1)) * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
(L,q,(abs (p + 1))) * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
q " is Element of the carrier of L
(q ") * (L,q,(- p)) is Element of the carrier of L
(L,q,(abs (p + 1))) * ((q ") * (L,q,(- p))) is Element of the carrier of L
(L,q,p) " is Element of the carrier of L
(q ") * ((L,q,p) ") is Element of the carrier of L
(L,q,(abs (p + 1))) * ((q ") * ((L,q,p) ")) is Element of the carrier of L
(L,q,(abs p)) " is Element of the carrier of L
(q ") * ((L,q,(abs p)) ") is Element of the carrier of L
(L,q,(abs (p + 1))) * ((q ") * ((L,q,(abs p)) ")) is Element of the carrier of L
q * (L,q,(abs p)) is Element of the carrier of L
(q * (L,q,(abs p))) " is Element of the carrier of L
(L,q,(abs (p + 1))) * ((q * (L,q,(abs p))) ") is Element of the carrier of L
(abs p) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(L,q,((abs p) + 1)) is Element of the carrier of L
(L,q,((abs p) + 1)) " is Element of the carrier of L
(L,q,(abs (p + 1))) * ((L,q,((abs p) + 1)) ") is Element of the carrier of L
(L,q,(abs (p + 1))) " is Element of the carrier of L
(L,q,(abs (p + 1))) * ((L,q,(abs (p + 1))) ") is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
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 L
(power L) . (q,m) is set
abs (p + 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,q,(abs (p + 1))) is Element of the carrier of L
q |^ (abs (p + 1)) is Element of the carrier of L
(power L) . (q,(abs (p + 1))) is set
(- 1) + 1 is V11() V12() integer ext-real set
(L,q,(- 1)) * (L,q,(- p)) is Element of the carrier of L
(L,q,(p + 1)) * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
(L,q,(abs (p + 1))) " is Element of the carrier of L
((L,q,(abs (p + 1))) ") * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
q " is Element of the carrier of L
(q ") * (L,q,(- p)) is Element of the carrier of L
((L,q,(abs (p + 1))) ") * ((q ") * (L,q,(- p))) is Element of the carrier of L
((L,q,(abs (p + 1))) ") * (q ") is Element of the carrier of L
(((L,q,(abs (p + 1))) ") * (q ")) * (L,q,(- p)) is Element of the carrier of L
(L,q,(abs (p + 1))) * q is Element of the carrier of L
((L,q,(abs (p + 1))) * q) " is Element of the carrier of L
(((L,q,(abs (p + 1))) * q) ") * (L,q,(- p)) is Element of the carrier of L
(abs (p + 1)) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(L,q,((abs (p + 1)) + 1)) is Element of the carrier of L
(L,q,((abs (p + 1)) + 1)) " is Element of the carrier of L
((L,q,((abs (p + 1)) + 1)) ") * (L,q,(- p)) is Element of the carrier of L
- (p + 1) is V11() V12() integer ext-real set
(- (p + 1)) + 1 is V11() V12() integer ext-real set
(L,q,((- (p + 1)) + 1)) is Element of the carrier of L
(L,q,((- (p + 1)) + 1)) " is Element of the carrier of L
((L,q,((- (p + 1)) + 1)) ") * (L,q,(- p)) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
q " is Element of the carrier of L
(L,q,(- 1)) * (L,q,(- p)) is Element of the carrier of L
(L,q,(p + 1)) * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(1. L) * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
(q ") * (L,q,(- p)) is Element of the carrier of L
(L,q,p) " is Element of the carrier of L
(q ") * ((L,q,p) ") is Element of the carrier of L
(q ") " is Element of the carrier of L
(q ") * ((q ") ") is Element of the carrier of L
(L,q,(- 1)) * (L,q,(- p)) is Element of the carrier of L
(L,q,(p + 1)) * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(L,q,(- 1)) * (L,q,(- p)) is Element of the carrier of L
(L,q,(p + 1)) * ((L,q,(- 1)) * (L,q,(- p))) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
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 L
(power L) . (q,m) is set
abs (p + 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q |^ (abs (p + 1)) is Element of the carrier of L
(power L) . (q,(abs (p + 1))) is set
(q |^ (abs (p + 1))) " is Element of the carrier of L
- (p + 1) is V11() V12() integer ext-real set
(L,q,(- (p + 1))) is Element of the carrier of L
(L,q,(p + 1)) * (L,q,(- (p + 1))) is Element of the carrier of L
(L,q,(p + 1)) " is Element of the carrier of L
(L,q,(p + 1)) * ((L,q,(p + 1)) ") is Element of the carrier of L
- (- (p + 1)) is V11() V12() integer ext-real set
(L,q,(- (- (p + 1)))) is Element of the carrier of L
((L,q,(- 1)) * (L,q,(- p))) " is Element of the carrier of L
(L,q,(- p)) " is Element of the carrier of L
(L,q,(- 1)) " is Element of the carrier of L
((L,q,(- p)) ") * ((L,q,(- 1)) ") is Element of the carrier of L
- (- p) is V11() V12() integer ext-real set
(L,q,(- (- p))) is Element of the carrier of L
(L,q,(- (- p))) * ((L,q,(- 1)) ") is Element of the carrier of L
- (- 1) is V11() V12() integer ext-real non negative set
(L,q,(- (- 1))) is Element of the carrier of L
(L,q,p) * (L,q,(- (- 1))) 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
0. L is V48(L) Element of the carrier of L
p is V11() V12() integer ext-real set
p - 1 is V11() V12() integer ext-real set
q is Element of the carrier of L
(L,q,(p - 1)) is Element of the carrier of L
(L,q,p) is Element of the carrier of L
(L,q,(- 1)) is Element of the carrier of L
(L,q,p) * (L,q,(- 1)) 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
q |^ m 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,m) is set
abs (p - 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q |^ (abs (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) . (q,(abs (p - 1))) is set
(q |^ (abs (p - 1))) " 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
- 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
(L,q,(abs (- p))) is Element of the carrier of L
q |^ (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) . (q,(abs (- p))) is set
1 + 0 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
abs (p - 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(abs (p - 1)) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(p - 1) + 1 is V11() V12() integer ext-real set
(L,q,(- p)) is Element of the carrier of L
q * (L,q,(- p)) is Element of the carrier of L
(L,q,(p - 1)) * (q * (L,q,(- p))) is Element of the carrier of L
(L,q,(p - 1)) * q is Element of the carrier of L
((L,q,(p - 1)) * q) * (L,q,(- p)) is Element of the carrier of L
(L,q,(abs (p - 1))) is Element of the carrier of L
(L,q,(abs (p - 1))) * q is Element of the carrier of L
((L,q,(abs (p - 1))) * q) * (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 - 1))) * q) * ((L,q,(abs (- p))) ") is Element of the carrier of L
(L,q,((abs (p - 1)) + 1)) is Element of the carrier of L
(L,q,((abs (p - 1)) + 1)) * ((L,q,(abs (- p))) ") is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
abs (p - 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,q,(abs (p - 1))) is Element of the carrier of L
q |^ (abs (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) . (q,(abs (p - 1))) is set
1 - p is V11() V12() integer ext-real set
- (p - 1) is V11() V12() integer ext-real set
- p is V11() V12() integer ext-real set
(L,q,(- p)) is Element of the carrier of L
q * (L,q,(- p)) is Element of the carrier of L
(L,q,(p - 1)) * (q * (L,q,(- p))) is Element of the carrier of L
(L,q,(abs (p - 1))) " is Element of the carrier of L
((L,q,(abs (p - 1))) ") * (q * (L,q,(- p))) 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,q,(abs (- p))) is Element of the carrier of L
q * (L,q,(abs (- p))) is Element of the carrier of L
((L,q,(abs (p - 1))) ") * (q * (L,q,(abs (- p)))) is Element of the carrier of L
1 + (abs (- p)) is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(L,q,(1 + (abs (- p)))) is Element of the carrier of L
((L,q,(abs (p - 1))) ") * (L,q,(1 + (abs (- p)))) is Element of the carrier of L
1 + (- p) is V11() V12() integer ext-real set
(L,q,(1 + (- p))) is Element of the carrier of L
((L,q,(abs (p - 1))) ") * (L,q,(1 + (- p))) is Element of the carrier of L
((L,q,(abs (p - 1))) ") * (L,q,(abs (p - 1))) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
- p is V11() V12() integer ext-real set
(L,q,(- p)) is Element of the carrier of L
q * (L,q,(- p)) is Element of the carrier of L
(L,q,(p - 1)) * (q * (L,q,(- p))) is Element of the carrier of L
q " is Element of the carrier of L
(q ") * (q * (L,q,(- p))) is Element of the carrier of L
(q ") * q is Element of the carrier of L
((q ") * q) * (L,q,(- p)) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(1. L) * (L,q,(- p)) is Element of the carrier of L
(L,q,0) is Element of the carrier of L
- p is V11() V12() integer ext-real set
(L,q,(- p)) is Element of the carrier of L
q * (L,q,(- p)) is Element of the carrier of L
(L,q,(p - 1)) * (q * (L,q,(- p))) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
- p is V11() V12() integer ext-real set
(L,q,(- p)) is Element of the carrier of L
q * (L,q,(- p)) is Element of the carrier of L
(L,q,(p - 1)) * (q * (L,q,(- p))) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
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 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,m) is set
abs (- p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q |^ (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) . (q,(abs (- p))) is set
(q |^ (abs (- p))) " 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
q |^ m 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,m) is set
abs (p - 1) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q |^ (abs (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) . (q,(abs (p - 1))) is set
(q |^ (abs (p - 1))) " is Element of the carrier of L
1 - p is V11() V12() integer ext-real set
(L,q,(1 - p)) is Element of the carrier of L
(L,q,(p - 1)) * (L,q,(1 - p)) is Element of the carrier of L
- (p - 1) is V11() V12() integer ext-real set
(L,q,(- (p - 1))) is Element of the carrier of L
(L,q,(p - 1)) * (L,q,(- (p - 1))) is Element of the carrier of L
(L,q,(p - 1)) " is Element of the carrier of L
(L,q,(p - 1)) * ((L,q,(p - 1)) ") is Element of the carrier of L
(L,q,(1 - p)) " is Element of the carrier of L
(L,q,(- p)) " is Element of the carrier of L
q " is Element of the carrier of L
((L,q,(- p)) ") * (q ") is Element of the carrier of L
- (- p) is V11() V12() integer ext-real set
(L,q,(- (- p))) is Element of the carrier of L
(L,q,(- (- p))) * (q ") is Element of the carrier of L
- (1 - p) is V11() V12() integer ext-real set
(L,q,(- (1 - p))) 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
0. L is V48(L) Element of the carrier of L
p is V11() V12() integer ext-real set
q is V11() V12() integer ext-real set
p + q is V11() V12() integer ext-real set
m is Element of the carrier of L
(L,m,p) is Element of the carrier of L
(L,m,q) is Element of the carrier of L
(L,m,p) * (L,m,q) is Element of the carrier of L
(L,m,(p + q)) is Element of the carrier of L
x is V11() V12() integer ext-real set
(L,m,x) is Element of the carrier of L
x - 1 is V11() V12() integer ext-real set
(L,m,(x - 1)) is Element of the carrier of L
x + 1 is V11() V12() integer ext-real set
(L,m,(x + 1)) is Element of the carrier of L
v1 is V11() V12() integer ext-real set
v1 + (x - 1) is V11() V12() integer ext-real set
(L,m,(v1 + (x - 1))) is Element of the carrier of L
(L,m,v1) is Element of the carrier of L
(L,m,v1) * (L,m,(x - 1)) is Element of the carrier of L
v1 - 1 is V11() V12() integer ext-real set
(v1 - 1) + x is V11() V12() integer ext-real set
(L,m,((v1 - 1) + x)) is Element of the carrier of L
(L,m,(v1 - 1)) is Element of the carrier of L
(L,m,(v1 - 1)) * (L,m,x) is Element of the carrier of L
(L,m,(- 1)) is Element of the carrier of L
(L,m,v1) * (L,m,(- 1)) is Element of the carrier of L
((L,m,v1) * (L,m,(- 1))) * (L,m,x) is Element of the carrier of L
(L,m,(- 1)) * (L,m,x) is Element of the carrier of L
(L,m,v1) * ((L,m,(- 1)) * (L,m,x)) is Element of the carrier of L
x + (- 1) is V11() V12() integer ext-real set
(L,m,(x + (- 1))) is Element of the carrier of L
(L,m,v1) * (L,m,(x + (- 1))) is Element of the carrier of L
v1 is V11() V12() integer ext-real set
v1 + (x + 1) is V11() V12() integer ext-real set
(L,m,(v1 + (x + 1))) is Element of the carrier of L
(L,m,v1) is Element of the carrier of L
(L,m,v1) * (L,m,(x + 1)) is Element of the carrier of L
v1 + 1 is V11() V12() integer ext-real set
(v1 + 1) + x is V11() V12() integer ext-real set
(L,m,((v1 + 1) + x)) is Element of the carrier of L
(L,m,(v1 + 1)) is Element of the carrier of L
(L,m,(v1 + 1)) * (L,m,x) is Element of the carrier of L
(L,m,1) is Element of the carrier of L
(L,m,v1) * (L,m,1) is Element of the carrier of L
((L,m,v1) * (L,m,1)) * (L,m,x) is Element of the carrier of L
(L,m,1) * (L,m,x) is Element of the carrier of L
(L,m,v1) * ((L,m,1) * (L,m,x)) is Element of the carrier of L
(L,m,0) is Element of the carrier of L
x is V11() V12() integer ext-real set
x + 0 is V11() V12() integer ext-real set
(L,m,(x + 0)) is Element of the carrier of L
(L,m,x) is Element of the carrier of L
(L,m,x) * (L,m,0) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(L,m,x) * (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 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 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 " 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 |^ p is Element of the carrier of L
(power L) . (q,p) is set
(q |^ p) " is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
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 L
(power L) . ((q "),m) is set
q |^ m is Element of the carrier of L
(power L) . (q,m) is set
(q |^ m) " 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
(q ") |^ (m + 1) is Element of the carrier of L
(power L) . ((q "),(m + 1)) is set
((q ") |^ m) * (q ") is Element of the carrier of L
q * (q |^ m) is Element of the carrier of L
(q * (q |^ m)) " is Element of the carrier of L
q |^ 1 is Element of the carrier of L
(power L) . (q,1) is set
(q |^ 1) * (q |^ m) is Element of the carrier of L
((q |^ 1) * (q |^ m)) " is Element of the carrier of L
q |^ (m + 1) is Element of the carrier of L
(power L) . (q,(m + 1)) is set
(q |^ (m + 1)) " is Element of the carrier of L
(q ") |^ 0 is Element of the carrier of L
(power L) . ((q "),0) is set
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) " is Element of the carrier of L
q |^ 0 is Element of the carrier of L
(power L) . (q,0) is set
(q |^ 0) " 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 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 V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
- p is V11() V12() integer ext-real non positive set
q is Element of the carrier of L
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
(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 |^ p is Element of the carrier of L
(power L) . (q,p) is set
(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
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
0. L is V48(L) Element of the carrier of L
p is Element of the carrier of L
q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
q - 1 is V11() V12() integer ext-real set
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
x - 1 is V11() V12() integer ext-real set
(q - 1) * (x - 1) is V11() V12() integer ext-real set
(L,p,((q - 1) * (x - 1))) 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 V11() V12() integer ext-real set
(m - 1) * (x - 1) is V11() V12() integer ext-real set
- ((m - 1) * (x - 1)) is V11() V12() integer ext-real set
(L,p,(- ((m - 1) * (x - 1)))) is Element of the carrier of L
(L,p,((q - 1) * (x - 1))) * (L,p,(- ((m - 1) * (x - 1)))) is Element of the carrier of L
q - m is V11() V12() integer ext-real set
(q - m) * (x - 1) is V11() V12() integer ext-real set
(L,p,((q - m) * (x - 1))) is Element of the carrier of L
((q - 1) * (x - 1)) + (- ((m - 1) * (x - 1))) is V11() V12() integer ext-real set
(L,p,(((q - 1) * (x - 1)) + (- ((m - 1) * (x - 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
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
m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q * m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,p,(q * m)) is Element of the carrier of L
(L,p,q) is Element of the carrier of L
(L,(L,p,q),m) is Element of the carrier of L
p |^ (q * m) 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 * m)) is set
p |^ q is Element of the carrier of L
(power L) . (p,q) is set
(p |^ q) |^ m is Element of the carrier of L
(power L) . ((p |^ q),m) is set
(L,(p |^ q),m) 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 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 Element of the carrier of L
p " is Element of the carrier of L
1. L is V48(L) 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,(p "),q) is Element of the carrier of L
(L,p,q) is Element of the carrier of L
(L,p,q) " is Element of the carrier of L
p |^ 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,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
(L,(p "),(q + 1)) is Element of the carrier of L
(p ") |^ (q + 1) is Element of the carrier of L
(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,(p "),q) * (p ") is Element of the carrier of L
(power L) . (p,q) is Element of the carrier of L
((power L) . (p,q)) " is Element of the carrier of L
(((power L) . (p,q)) ") * (p ") is Element of the carrier of L
p * (p |^ q) is Element of the carrier of L
(p * (p |^ q)) " is Element of the carrier of L
p |^ 1 is Element of the carrier of L
(power L) . (p,1) is set
(p |^ 1) * (p |^ q) is Element of the carrier of L
((p |^ 1) * (p |^ q)) " is Element of the carrier of L
p |^ (q + 1) is Element of the carrier of L
(power L) . (p,(q + 1)) is set
(p |^ (q + 1)) " is Element of the carrier of L
(L,p,(q + 1)) is Element of the carrier of L
(L,p,(q + 1)) " 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,(p "),q) is Element of the carrier of L
(L,p,q) is Element of the carrier of L
(L,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,(p "),(q + 1)) is Element of the carrier of L
(L,p,(q + 1)) is Element of the carrier of L
(L,p,(q + 1)) " 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,(p "),q) is Element of the carrier of L
(L,p,q) is Element of the carrier of L
(L,p,q) " is Element of the carrier of L
(L,(p "),0) 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
(L,p,0) is Element of the carrier of L
(L,p,0) " 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
0. L is V48(L) Element of the carrier of L
p is Element of the carrier of L
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
(L,p,q) is Element of the carrier of L
(L,p,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
(L,p,m) is Element of the carrier of L
(L,p,m) " 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
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 set
(L,(p "),(abs q)) is Element of the carrier of L
(L,(p "),(abs q)) " is Element of the carrier of L
(p ") " is Element of the carrier of L
(L,((p ") "),(abs q)) is Element of the carrier of L
(L,p,(abs q)) " is Element of the carrier of L
((L,p,(abs q)) ") " 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
0. L is V48(L) Element of the carrier of L
p is Element of the carrier of L
q is V11() V12() integer ext-real set
m is V11() V12() integer ext-real set
q * m is V11() V12() integer ext-real set
(L,p,(q * m)) is Element of the carrier of L
(L,p,q) is Element of the carrier of L
(L,(L,p,q),m) is Element of the carrier of L
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,p,x) is Element of the carrier of L
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,(L,p,x),v1) is Element of the carrier of L
- m 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
p |^ x 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,x) is set
abs m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,p,q) |^ (abs m) is Element of the carrier of L
(power L) . ((L,p,q),(abs m)) is set
((L,p,q) |^ (abs m)) " is Element of the carrier of L
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q * v1 is V11() V12() integer ext-real set
- (q * v1) is V11() V12() integer ext-real set
(L,p,(q * v1)) is Element of the carrier of L
(L,p,(q * v1)) " is Element of the carrier of L
p " is Element of the carrier of L
(L,(p "),(q * v1)) is Element of the carrier of L
(L,(p "),x) is Element of the carrier of L
(L,(L,(p "),x),v1) is Element of the carrier of L
(L,p,q) " is Element of the carrier of L
(L,((L,p,q) "),v1) is Element of the carrier of L
(L,((L,p,q) "),m) is Element of the carrier of L
(L,((L,p,q) "),m) " is Element of the carrier of L
(L,(L,p,q),m) " is Element of the carrier of L
((L,(L,p,q),m) ") " is Element of the carrier of L
- q is V11() V12() integer ext-real set
abs q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
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 set
(p |^ (abs q)) " is Element of the carrier of L
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
x * m is V11() V12() integer ext-real set
- (x * m) is V11() V12() integer ext-real set
(L,p,(x * m)) is Element of the carrier of L
(L,p,(x * m)) " is Element of the carrier of L
p " is Element of the carrier of L
(L,(p "),(x * m)) is Element of the carrier of L
(L,(p "),x) is Element of the carrier of L
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,(L,(p "),x),v1) is Element of the carrier of L
(L,(p "),q) is Element of the carrier of L
(L,(p "),q) " is Element of the carrier of L
(L,((L,(p "),q) "),v1) is Element of the carrier of L
(L,p,q) " is Element of the carrier of L
((L,p,q) ") " is Element of the carrier of L
(L,(((L,p,q) ") "),m) is Element of the carrier of L
- q is V11() V12() integer ext-real set
- m is V11() V12() integer ext-real set
(L,p,(- q)) is Element of the carrier of L
x 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
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,x) is set
p " 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
(p ") |^ (abs q) is Element of the carrier of L
(power L) . ((p "),(abs q)) is set
(L,(p "),q) is Element of the carrier of L
((p ") |^ (abs q)) " is Element of the carrier of L
(- 1) * (- 1) is V11() V12() integer ext-real non negative set
(q * m) * ((- 1) * (- 1)) is V11() V12() integer ext-real set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
x * v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,p,x) is Element of the carrier of L
(L,(L,p,x),v1) is Element of the carrier of L
(L,(L,p,(- q)),m) is Element of the carrier of L
(L,(L,p,(- q)),m) " is Element of the carrier of L
(L,p,q) " is Element of the carrier of L
(L,((L,p,q) "),m) is Element of the carrier of L
(L,((L,p,q) "),m) " is Element of the carrier of L
(L,(L,(p "),q),m) is Element of the carrier of L
(L,(L,(p "),q),m) " is Element of the carrier of L
(L,(p "),q) " is Element of the carrier of L
(L,((L,(p "),q) "),m) is Element of the carrier of L
(p ") " is Element of the carrier of L
(L,((p ") "),q) is Element of the carrier of L
(L,(L,((p ") "),q),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
p 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
q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m - 1 is V11() V12() integer ext-real set
q * (m - 1) is V11() V12() integer ext-real set
(L,p,(q * (m - 1))) is Element of the carrier of L
p |^ 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,q) is set
(L,(p |^ q),(m - 1)) is Element of the carrier of L
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q * x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
p |^ (q * x) is Element of the carrier of L
(power L) . (p,(q * x)) is set
(p |^ q) |^ x is Element of the carrier of L
(power L) . ((p |^ q),x) is set
(L,(p |^ q),x) 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
1. L is Element of the carrier of L
p is Element of the carrier of 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
p |^ 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,q) is set
(p ") |^ q is Element of the carrier of L
(power L) . ((p "),q) is set
(1. L) * ((p ") |^ 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
0. L is V48(L) Element of the carrier of L
1. L is V48(L) Element of the carrier of L
p is Element of the carrier of 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
(p ") |^ 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 "),q) is set
p |^ q is Element of the carrier of L
(power L) . (p,q) is set
1_ L is Element of the carrier of L
p |^ 0 is Element of the carrier of L
(power L) . (p,0) is set
((p ") |^ q) * (1. L) is Element of the carrier of L
((p ") |^ q) * (p |^ 0) is Element of the carrier of L
((p ") |^ q) * (p |^ q) is Element of the carrier of L
p is non empty ZeroStr
the carrier of p is non empty set
K7(NAT, the carrier of p) is V32() set
K6(K7(NAT, the carrier of p)) is V32() set
the carrier of p * is FinSequenceSet of the carrier of p
L is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
q is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
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
[:(Seg m),(Seg 1):] 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
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[x,v1] is V26() set
x - 1 is V11() V12() integer ext-real set
q . (x - 1) is set
q /. (x - 1) is Element of the carrier of p
[x,v1] `1 is set
Seg 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 <= L ) } is set
dom q is set
1 - 1 is V11() V12() integer ext-real set
x is Relation-like NAT -defined the carrier of p * -valued Function-like FinSequence-like tabular Matrix of m,1, the carrier of p
Indices x is set
dom x is Element of K6(NAT)
width x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of 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
K7((dom x),(Seg (width x))) is set
v1 is Relation-like NAT -defined the carrier of p * -valued Function-like FinSequence-like tabular Matrix of L,1, the carrier of p
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
Seg 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 <= L ) } is set
Indices v1 is set
dom v1 is Element of K6(NAT)
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
K7((dom v1),(Seg (width v1))) is set
[:(Seg L),(Seg 1):] is Relation-like NAT -defined NAT -valued Element of K6(K7(NAT,NAT))
[v2,1] is V26() set
v1 * (v2,1) is Element of the carrier of p
v2 - 1 is V11() V12() integer ext-real set
q . (v2 - 1) is set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 * (v2,1) is Element of the carrier of p
v2 - 1 is V11() V12() integer ext-real set
q . (v2 - 1) is set
m is Relation-like NAT -defined the carrier of p * -valued Function-like FinSequence-like tabular Matrix of L,1, the carrier of p
x is Relation-like NAT -defined the carrier of p * -valued Function-like FinSequence-like tabular Matrix of L,1, the carrier of p
Indices m is set
dom m is Element of K6(NAT)
width m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width 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 <= width m ) } is set
K7((dom m),(Seg (width m))) is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[v1,v2] is V26() set
m * (v1,v2) is Element of the carrier of p
x * (v1,v2) is Element of the carrier of p
width x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len m 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
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[v1,v2] is V26() set
Indices m is set
dom m is Element of K6(NAT)
width m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width 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 <= width m ) } is set
K7((dom m),(Seg (width m))) is set
Seg 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 <= L ) } is set
[:(Seg L),(Seg 1):] 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
[v1,v2] `2 is set
[v1,v2] `1 is set
m * (v1,v2) is Element of the carrier of p
v1 - 1 is V11() V12() integer ext-real set
q . (v1 - 1) is set
x * (v1,v2) is Element of the carrier of p
width x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len m 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
L is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
p is non empty ZeroStr
the carrier of p is non empty set
K7(NAT, the carrier of p) is V32() set
K6(K7(NAT, the carrier of p)) is V32() set
q is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
(L,p,q) is Relation-like NAT -defined the carrier of p * -valued Function-like FinSequence-like tabular Matrix of L,1, the carrier of p
the carrier of p * is FinSequenceSet of the carrier of p
len (L,p,q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width (L,p,q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
0 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive 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
(L,p,q) * ((x + 1),1) is Element of the carrier of p
(x + 1) - 1 is V11() V12() integer ext-real set
q . ((x + 1) - 1) is set
q . x is Element of the carrier of p
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
x + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(L,p,q) * ((x + 1),1) is Element of the carrier of p
q . x is Element of the carrier of p
L is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
p is non empty ZeroStr
the carrier of p is non empty set
K7(NAT, the carrier of p) is V32() set
K6(K7(NAT, the carrier of p)) is V32() set
the carrier of p * is FinSequenceSet of the carrier of p
q is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
(L,p,q) is Relation-like NAT -defined the carrier of p * -valued Function-like FinSequence-like tabular Matrix of L,1, the carrier of p
m is Relation-like NAT -defined the carrier of p * -valued Function-like FinSequence-like tabular Matrix of L,1, the carrier of p
width (L,p,q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Indices (L,p,q) is set
dom (L,p,q) is Element of K6(NAT)
Seg (width (L,p,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 <= width (L,p,q) ) } is set
K7((dom (L,p,q)),(Seg (width (L,p,q)))) is set
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[x,v1] is V26() set
(L,p,q) * (x,v1) is Element of the carrier of p
m * (x,v1) is Element of the carrier of p
len (L,p,q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg 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 <= L ) } is set
x - 1 is V11() V12() integer ext-real set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
m * ((v2 + 1),1) is Element of the carrier of p
q . v2 is Element of the carrier of p
(L,p,q) * ((v2 + 1),1) is Element of the carrier of p
len (L,p,q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len m 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
the carrier of L * is FinSequenceSet of the carrier of L
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 FinSequence-like tabular 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
0. L is V48(L) Element of the carrier of L
q is set
m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
p * ((m + 1),1) 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 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) Element of K6(K7(NAT, 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 V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
m . x is Element of the carrier of L
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
p * ((v1 + 1),1) is Element of the carrier of L
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
m . x is Element of the carrier of L
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 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 V29( NAT , the carrier of L) finite-Support Element of K6(K7(NAT, the carrier of L))
x . v1 is Element of the carrier of L
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
v2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
p * ((v2 + 1),1) 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
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
p * ((v1 + 1),1) is Element of the carrier of L
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
v2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
p * ((v2 + 1),1) 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
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
p * ((v1 + 1),1) is Element of the carrier of L
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
x . v2 is Element of 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))
m 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))
x is set
dom q is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q . x is set
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
p * ((v1 + 1),1) is Element of the carrier of L
m . x is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
q . x is set
m . x is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom m is set
L is non empty unital right_unital well-unital left_unital doubleLoopStr
the carrier of L is non empty set
L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable unital right-distributive right_unital well-unital left_unital add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr
0. L is V48(L) Element of the carrier of L
the carrier of L is non empty non trivial set
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 set
(0. L) |^ 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) . ((0. 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
(0. L) |^ (q + 1) is Element of the carrier of L
(power L) . ((0. L),(q + 1)) is set
((0. L) |^ q) * (0. L) is Element of the carrier of L
(0. L) |^ 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) . ((0. L),1) is set
p + 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
(0. L) |^ p is Element of the carrier of L
(power L) . ((0. L),p) is set
1. L is V48(L) 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 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
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 " is Element of the carrier of L
0. L is V48(L) Element of the carrier of L
1. L is V48(L) Element of the carrier of L
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 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 "),m) is set
q |^ m is Element of the carrier of L
(power L) . (q,m) is set
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 ") |^ p is Element of the carrier of L
(power L) . ((q "),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
1. L is V48(L) 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
0. L is V48(L) Element of the carrier of L
m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
m - x is V11() V12() integer ext-real set
(L,q,(m - x)) is Element of the carrier of L
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m - 1 is V11() V12() integer ext-real set
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(m - 1) + 1 is V11() V12() integer ext-real set
x - x is V11() V12() integer ext-real set
q |^ v1 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,v1) is set
x - m is V11() V12() integer ext-real set
m - m is V11() V12() integer ext-real set
x - x is V11() V12() integer ext-real set
abs (m - x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
- (m - x) is V11() V12() integer ext-real set
x - 1 is V11() V12() integer ext-real set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(x - 1) + 1 is V11() V12() integer ext-real set
q |^ v1 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,v1) is set
(q |^ v1) " is Element of the carrier of L
(q |^ v1) * (1. L) is Element of the carrier of L
p is non empty unital right_unital well-unital left_unital doubleLoopStr
the carrier of p is non empty set
K7(NAT, the carrier of p) is V32() set
K6(K7(NAT, the carrier of p)) is V32() set
L is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
q is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
m is Element of the carrier of p
0. p is V48(p) Element of the carrier of p
x is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m |^ v1 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) . (m,v1) is set
eval (q,(m |^ v1)) is Element of the carrier of p
v1 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
x is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) Element of K6(K7(NAT, the carrier of p))
v1 is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) Element of K6(K7(NAT, the carrier of p))
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 . u9 is Element of the carrier of p
u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m |^ u 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) . (m,u) is set
eval (q,(m |^ u)) is Element of the carrier of p
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 . u9 is Element of the carrier of p
u9 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 is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
v2 . u9 is Element of the carrier of p
u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m |^ u 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) . (m,u) is set
eval (q,(m |^ u)) is Element of the carrier of p
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 . u9 is Element of the carrier of p
m |^ u9 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) . (m,u9) is set
eval (q,(m |^ u9)) is Element of the carrier of p
u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m |^ u is Element of the carrier of p
(power p) . (m,u) is set
eval (q,(m |^ u)) is Element of the carrier of p
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 . u9 is Element of the carrier of p
m |^ u9 is Element of the carrier of p
(power p) . (m,u9) is set
eval (q,(m |^ u9)) is Element of the carrier of p
u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 . u is Element of the carrier of p
x is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
v1 is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
v2 is set
dom x is set
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
x . v2 is set
m |^ u9 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) . (m,u9) is set
eval (q,(m |^ u9)) is Element of the carrier of p
v1 . v2 is set
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
x . v2 is set
v1 . v2 is set
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom v1 is set
L is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
p is non empty unital right_unital well-unital left_unital doubleLoopStr
the carrier of p is non empty set
0_. p is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
K7(NAT, the carrier of p) is V32() set
K6(K7(NAT, the carrier of p)) is V32() set
0. p is V48(p) Element of the carrier of p
K391( the carrier of p,NAT,(0. p)) is V8() Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) Element of K6(K7(NAT, the carrier of p))
q is Element of the carrier of p
(L,p,(0_. p),q) is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
x is set
dom (L,p,(0_. p),q) is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,p,(0_. p),q) . x is set
q |^ v1 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,v1) is set
eval ((0_. p),(q |^ v1)) is Element of the carrier of p
(0_. p) . v1 is Element of the carrier of p
(0_. p) . x is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,p,(0_. p),q) . x is set
(0_. p) . v1 is Element of the carrier of p
(0_. p) . x is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom (0_. p) is set
L is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
p 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 p is non empty non trivial set
K7(NAT, the carrier of p) is V32() set
K6(K7(NAT, the carrier of p)) is V32() set
q is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
m is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
q *' m is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
x is Element of the carrier of p
(L,p,q,x) is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
(L,p,m,x) is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
(p,(L,p,q,x),(L,p,m,x)) is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
(L,p,(q *' m),x) is Relation-like NAT -defined the carrier of p -valued Function-like V29( NAT , the carrier of p) finite-Support Element of K6(K7(NAT, the carrier of p))
u is set
dom (p,(L,p,q,x),(L,p,m,x)) is set
k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,p,(q *' m),x) . u is set
x |^ k 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) . (x,k) is set
eval ((q *' m),(x |^ k)) is Element of the carrier of p
eval (q,(x |^ k)) is Element of the carrier of p
eval (m,(x |^ k)) is Element of the carrier of p
(eval (q,(x |^ k))) * (eval (m,(x |^ k))) is Element of the carrier of p
(L,p,q,x) . k is Element of the carrier of p
((L,p,q,x) . k) * (eval (m,(x |^ k))) is Element of the carrier of p
(L,p,m,x) . k is Element of the carrier of p
((L,p,q,x) . k) * ((L,p,m,x) . k) is Element of the carrier of p
(p,(L,p,q,x),(L,p,m,x)) . u is set
k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(p,(L,p,q,x),(L,p,m,x)) . u is set
(L,p,q,x) . k is Element of the carrier of p
(L,p,m,x) . k is Element of the carrier of p
((L,p,q,x) . k) * ((L,p,m,x) . k) is Element of the carrier of p
0. p is V48(p) Element of the carrier of p
(0. p) * ((L,p,m,x) . k) is Element of the carrier of p
(L,p,(q *' m),x) . u is set
k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom (L,p,(q *' m),x) 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
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 set
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
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
[:(Seg m),(Seg m):] 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
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[x,v1] is V26() set
x - 1 is V11() V12() integer ext-real set
v1 - 1 is V11() V12() integer ext-real set
(x - 1) * (v1 - 1) is V11() V12() integer ext-real set
(L,q,((x - 1) * (v1 - 1))) 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 m,m, the carrier of L
Indices x is set
dom x is Element of K6(NAT)
width x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of 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
K7((dom x),(Seg (width x))) is set
v1 is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
Indices v1 is set
dom v1 is Element of K6(NAT)
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
K7((dom v1),(Seg (width v1))) 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
[:(Seg p),(Seg p):] is Relation-like NAT -defined NAT -valued Element of K6(K7(NAT,NAT))
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[v2,u9] is V26() set
v1 * (v2,u9) is Element of the carrier of L
v2 - 1 is V11() V12() integer ext-real set
u9 - 1 is V11() V12() integer ext-real set
(v2 - 1) * (u9 - 1) is V11() V12() integer ext-real set
(L,q,((v2 - 1) * (u9 - 1))) is Element of the carrier of L
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
v1 * (v2,u9) is Element of the carrier of L
v2 - 1 is V11() V12() integer ext-real set
u9 - 1 is V11() V12() integer ext-real set
(v2 - 1) * (u9 - 1) is V11() V12() integer ext-real set
(L,q,((v2 - 1) * (u9 - 1))) is Element of the carrier of L
m is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
x is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
Indices m is set
dom m is Element of K6(NAT)
width m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width 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 <= width m ) } is set
K7((dom m),(Seg (width m))) 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
[:(Seg p),(Seg p):] 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
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[v1,v2] is V26() set
u9 is set
u is set
[u9,u] is V26() set
u9 is set
u is set
[u9,u] is V26() set
m * (v1,v2) is Element of the carrier of L
v1 - 1 is V11() V12() integer ext-real set
v2 - 1 is V11() V12() integer ext-real set
(v1 - 1) * (v2 - 1) is V11() V12() integer ext-real set
(L,q,((v1 - 1) * (v2 - 1))) is Element of the carrier of L
x * (v1,v2) 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
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 set
q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
1. (L,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
m is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,q, the carrier of L
(1. (L,p)) * m is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
width (1. (L,p)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (1. (L,p)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((1. (L,p)) * m) 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
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[v1,v2] is V26() set
Indices m is set
dom m is Element of K6(NAT)
width m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width 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 <= width m ) } is set
K7((dom m),(Seg (width m))) is set
Seg (len 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 <= len m ) } is set
dom ((1. (L,p)) * m) is Element of K6(NAT)
Indices ((1. (L,p)) * m) is set
width ((1. (L,p)) * m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width ((1. (L,p)) * 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 <= width ((1. (L,p)) * m) ) } is set
K7((dom ((1. (L,p)) * m)),(Seg (width ((1. (L,p)) * m)))) is set
((1. (L,p)) * m) * (v1,v2) is Element of the carrier of L
Line ((1. (L,p)),v1) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (width (1. (L,p))) -tuples_on the carrier of L
(width (1. (L,p))) -tuples_on the carrier of L is FinSequenceSet of the carrier of L
Col (m,v2) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (len m) -tuples_on the carrier of L
(len m) -tuples_on the carrier of L is FinSequenceSet of the carrier of L
(Line ((1. (L,p)),v1)) "*" (Col (m,v2)) is Element of the carrier of L
mlt ((Line ((1. (L,p)),v1)),(Col (m,v2))) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
Sum (mlt ((Line ((1. (L,p)),v1)),(Col (m,v2)))) is Element of the carrier of L
len (Line ((1. (L,p)),v1)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom (Line ((1. (L,p)),v1)) is Element of K6(NAT)
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 (1. (L,p)) is set
dom (1. (L,p)) is Element of K6(NAT)
Seg (width (1. (L,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 <= width (1. (L,p)) ) } is set
K7((dom (1. (L,p))),(Seg (width (1. (L,p))))) is set
[:(Seg p),(Seg p):] 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
[v1,v1] is V26() set
0. L is V48(L) Element of the carrier of L
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
(Line ((1. (L,p)),v1)) . u9 is set
[v1,u9] is V26() set
(1. (L,p)) * (v1,u9) is Element of the carrier of L
len (Col (m,v2)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom (Col (m,v2)) is Element of K6(NAT)
(Line ((1. (L,p)),v1)) . v1 is set
(1. (L,p)) * (v1,v1) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(Col (m,v2)) . v1 is set
m * (v1,v2) 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
(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
q is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
m is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
q * m is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
x is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, 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 *
Indices (q * m) is set
dom (q * m) is Element of K6(NAT)
width (q * m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width (q * 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 <= width (q * m) ) } is set
K7((dom (q * m)),(Seg (width (q * m)))) is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
[v1,v2] is V26() set
(q * m) * (v1,v2) is Element of the carrier of L
((L,p) * x) * (v1,v2) is Element of the carrier of L
width q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
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
len (q * m) 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
[:(Seg p),(Seg p):] 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
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
[:(Seg p),(Seg p):] 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
Indices x is set
dom x is Element of K6(NAT)
width x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of 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
K7((dom x),(Seg (width x))) is set
x * (v1,v2) is Element of the carrier of L
(L,p) * (x * (v1,v2)) is Element of the carrier of L
width ((L,p) * x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width q is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (q * m) 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
len ((L,p) * x) 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
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
K7(NAT, the carrier of L) is V32() set
K6(K7(NAT, the carrier of L)) is V32() set
p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
2 * p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
1. (L,(2 * p)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of 2 * p,2 * p, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
(L,(2 * p)) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(2 * 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(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) . ((2 * p),(1. L)) is Element of 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))
m 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 *' m 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))
((2 * p),L,(q *' m)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of 2 * p,1, the carrier of L
(1. (L,(2 * p))) * ((2 * p),L,(q *' m)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,(2 * p)) * ((1. (L,(2 * p))) * ((2 * p),L,(q *' m))) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,(2 * p)) * ((2 * p),L,(q *' m)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
2 * 0 is empty V4() V5() V6() V8() V9() V10() V11() V12() integer V32() V37() V39( {} ) ext-real non positive non negative Element of NAT
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
p is Element of the carrier of L
p " 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
v1 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
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m - x is V11() V12() integer ext-real set
(L,v1,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of v1,v1, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
(L,v1,(p ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of v1,v1, the carrier of L
(L,v1,p) * (L,v1,(p ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
((L,v1,p) * (L,v1,(p "))) * (m,x) is Element of the carrier of L
Line ((L,v1,p),m) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (width (L,v1,p)) -tuples_on the carrier of L
width (L,v1,p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(width (L,v1,p)) -tuples_on the carrier of L is FinSequenceSet of the carrier of L
len (Line ((L,v1,p),m)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (L,v1,(p ")) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Col ((L,v1,(p ")),x) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (len (L,v1,(p "))) -tuples_on the carrier of L
(len (L,v1,(p "))) -tuples_on the carrier of L is FinSequenceSet of the carrier of L
len (Col ((L,v1,(p ")),x)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x))) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
len (mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
0. L is V48(L) Element of the carrier of L
Seg 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 <= v1 ) } is set
dom (Col ((L,v1,(p ")),x)) is Element of K6(NAT)
dom (Line ((L,v1,p),m)) is Element of K6(NAT)
1 - 1 is V11() V12() integer ext-real set
x - 1 is V11() V12() integer ext-real set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
(Line ((L,v1,p),m)) /. v2 is Element of the carrier of L
(Col ((L,v1,(p ")),x)) /. v2 is Element of the carrier of L
((Line ((L,v1,p),m)) /. v2) * ((Col ((L,v1,(p ")),x)) /. v2) is Element of the carrier of L
v2 - 1 is V11() V12() integer ext-real set
(m - x) * (v2 - 1) is V11() V12() integer ext-real set
(L,p,((m - x) * (v2 - 1))) is Element of the carrier of L
dom (L,v1,(p ")) is Element of K6(NAT)
(Line ((L,v1,p),m)) . v2 is set
(x - 1) * (v2 - 1) is V11() V12() integer ext-real set
Seg (width (L,v1,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 <= width (L,v1,p) ) } is set
(L,v1,p) * (m,v2) is Element of the carrier of L
(Col ((L,v1,(p ")),x)) . v2 is set
(L,v1,(p ")) * (v2,x) is Element of the carrier of L
(L,(p "),((x - 1) * (v2 - 1))) is Element of the carrier of L
- ((x - 1) * (v2 - 1)) is V11() V12() integer ext-real set
(L,p,(- ((x - 1) * (v2 - 1)))) is Element of the carrier of L
m - 1 is V11() V12() integer ext-real set
(m - 1) * (v2 - 1) is V11() V12() integer ext-real set
(L,p,((m - 1) * (v2 - 1))) is Element of the carrier of L
(L,p,((m - 1) * (v2 - 1))) * (L,p,(- ((x - 1) * (v2 - 1)))) is Element of the carrier of L
Seg 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 <= v1 ) } is set
dom (Col ((L,v1,(p ")),x)) is Element of K6(NAT)
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
(mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) /. v2 is Element of the carrier of L
q /. v2 is Element of the carrier of L
dom (Line ((L,v1,p),m)) is Element of K6(NAT)
(Line ((L,v1,p),m)) /. v2 is Element of the carrier of L
(Col ((L,v1,(p ")),x)) /. v2 is Element of the carrier of L
((Line ((L,v1,p),m)) /. v2) * ((Col ((L,v1,(p ")),x)) /. v2) is Element of the carrier of L
v2 - 1 is V11() V12() integer ext-real set
(m - x) * (v2 - 1) is V11() V12() integer ext-real set
(L,p,((m - x) * (v2 - 1))) is Element of the carrier of L
(Col ((L,v1,(p ")),x)) . v2 is set
dom (mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) is Element of K6(NAT)
(Line ((L,v1,p),m)) . v2 is set
(mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) . v2 is set
dom (mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) is Element of K6(NAT)
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
(mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) . v2 is set
q . v2 is set
Seg 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 <= v1 ) } is set
dom q is Element of K6(NAT)
(mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) /. v2 is Element of the carrier of L
q /. v2 is Element of the carrier of L
Seg 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 <= v1 ) } is set
dom q is Element of K6(NAT)
Sum (mlt ((Line ((L,v1,p),m)),(Col ((L,v1,(p ")),x)))) is Element of the carrier of L
len (L,v1,p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((L,v1,p) * (L,v1,(p "))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width (L,v1,(p ")) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width ((L,v1,p) * (L,v1,(p "))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Indices ((L,v1,p) * (L,v1,(p "))) is set
dom ((L,v1,p) * (L,v1,(p "))) is Element of K6(NAT)
Seg (width ((L,v1,p) * (L,v1,(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 <= width ((L,v1,p) * (L,v1,(p "))) ) } is set
K7((dom ((L,v1,p) * (L,v1,(p ")))),(Seg (width ((L,v1,p) * (L,v1,(p ")))))) is set
[:(Seg v1),(Seg v1):] 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
[m,x] is V26() set
(Line ((L,v1,p),m)) "*" (Col ((L,v1,(p ")),x)) 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
0. L is V48(L) Element of the carrier of L
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
p 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
(L,p,x) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
x " is Element of the carrier of L
(L,p,(x ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
(L,p,x) * (L,p,(x ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
((L,p,x) * (L,p,(x "))) * (q,m) is Element of the carrier of L
q - m is V11() V12() integer ext-real set
p * (q - m) is V11() V12() integer ext-real set
(L,x,(p * (q - m))) is Element of the carrier of L
(L,x,p) is Element of the carrier of L
(L,(L,x,p),(q - m)) is Element of the carrier of L
x |^ 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) . (x,p) is set
(L,(x |^ p),(q - m)) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(L,(1. L),(q - m)) is Element of the carrier of L
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
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 - 1 is V11() V12() integer ext-real set
(q - m) * (v1 - 1) is V11() V12() integer ext-real set
(L,x,((q - m) * (v1 - 1))) is Element of the carrier of L
v1 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom v1 is Element of K6(NAT)
v1 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom v1 is Element of K6(NAT)
v1 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom v1 is Element of K6(NAT)
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 /. v2 is Element of the carrier of L
v2 - 1 is V11() V12() integer ext-real set
(q - m) * (v2 - 1) is V11() V12() integer ext-real set
(L,x,((q - m) * (v2 - 1))) is Element of the carrier of L
v1 . v2 is set
(L,x,(q - m)) is Element of the carrier of L
v2 is Element of the carrier of L
len v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 . u9 is set
u9 -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,x,(q - m)) |^ (u9 -' 1) is Element of the carrier of L
(power L) . ((L,x,(q - m)),(u9 -' 1)) is set
1 - 1 is V11() V12() integer ext-real set
u9 - 1 is V11() V12() integer ext-real set
v1 /. u9 is Element of the carrier of L
(q - m) * (u9 - 1) is V11() V12() integer ext-real set
(L,x,((q - m) * (u9 - 1))) is Element of the carrier of L
(q - m) * (u9 -' 1) is V11() V12() integer ext-real set
(L,x,((q - m) * (u9 -' 1))) is Element of the carrier of L
(L,(L,x,(q - m)),(u9 -' 1)) is Element of the carrier of L
Sum v1 is Element of the carrier of L
(L,x,(q - m)) |^ (len v1) is Element of the carrier of L
(power L) . ((L,x,(q - m)),(len v1)) is set
(1. L) - ((L,x,(q - m)) |^ (len v1)) is Element of the carrier of L
- ((L,x,(q - m)) |^ (len v1)) is Element of the carrier of L
(1. L) + (- ((L,x,(q - m)) |^ (len v1))) is Element of the carrier of L
(1. L) - (L,x,(q - m)) is Element of the carrier of L
- (L,x,(q - m)) is Element of the carrier of L
(1. L) + (- (L,x,(q - m))) is Element of the carrier of L
((1. L) - ((L,x,(q - m)) |^ (len v1))) / ((1. L) - (L,x,(q - m))) is Element of the carrier of L
((1. L) - (L,x,(q - m))) " is Element of the carrier of L
((1. L) - ((L,x,(q - m)) |^ (len v1))) * (((1. L) - (L,x,(q - m))) ") is Element of the carrier of L
(L,x,(q - m)) |^ p is Element of the carrier of L
(power L) . ((L,x,(q - m)),p) is set
(1. L) - ((L,x,(q - m)) |^ p) is Element of the carrier of L
- ((L,x,(q - m)) |^ p) is Element of the carrier of L
(1. L) + (- ((L,x,(q - m)) |^ p)) is Element of the carrier of L
((1. L) - ((L,x,(q - m)) |^ p)) / ((1. L) - (L,x,(q - m))) is Element of the carrier of L
((1. L) - ((L,x,(q - m)) |^ p)) * (((1. L) - (L,x,(q - m))) ") is Element of the carrier of L
(L,(L,x,(q - m)),p) is Element of the carrier of L
(1. L) - (L,(L,x,(q - m)),p) is Element of the carrier of L
- (L,(L,x,(q - m)),p) is Element of the carrier of L
(1. L) + (- (L,(L,x,(q - m)),p)) is Element of the carrier of L
((1. L) - (L,(L,x,(q - m)),p)) / ((1. L) - (L,x,(q - m))) is Element of the carrier of L
((1. L) - (L,(L,x,(q - m)),p)) * (((1. L) - (L,x,(q - m))) ") is Element of the carrier of L
(q - m) * p is V11() V12() integer ext-real set
(L,x,((q - m) * p)) is Element of the carrier of L
(1. L) - (L,x,((q - m) * p)) is Element of the carrier of L
- (L,x,((q - m) * p)) is Element of the carrier of L
(1. L) + (- (L,x,((q - m) * p))) is Element of the carrier of L
((1. L) - (L,x,((q - m) * p))) / ((1. L) - (L,x,(q - m))) is Element of the carrier of L
((1. L) - (L,x,((q - m) * p))) * (((1. L) - (L,x,(q - m))) ") is Element of the carrier of L
(1. L) - v2 is Element of the carrier of L
- v2 is Element of the carrier of L
(1. L) + (- v2) is Element of the carrier of L
(0. L) / ((1. L) - v2) is Element of the carrier of L
((1. L) - v2) " is Element of the carrier of L
(0. L) * (((1. L) - v2) ") 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
p is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
1. (L,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
(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
(L,p) * (1. (L,p)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
q is Element of the carrier of L
(L,p,q) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
q " is Element of the carrier of L
(L,p,(q ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
(L,p,q) * (L,p,(q ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
x is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
((L,p,q) * (L,p,(q "))) * (m,x) is Element of the carrier of L
(1. (L,p)) * (m,x) is Element of the carrier of L
(L,p) * ((1. (L,p)) * (m,x)) is Element of the carrier of L
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
m - x is V11() V12() integer ext-real set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 - 1 is V11() V12() integer ext-real set
(m - x) * (v1 - 1) is V11() V12() integer ext-real set
(L,q,((m - x) * (v1 - 1))) is Element of the carrier of L
v1 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom v1 is Element of K6(NAT)
v1 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom v1 is Element of K6(NAT)
v1 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom v1 is Element of K6(NAT)
len 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
v1 /. v2 is Element of the carrier of L
v2 - 1 is V11() V12() integer ext-real set
(m - x) * (v2 - 1) is V11() V12() integer ext-real set
(L,q,((m - x) * (v2 - 1))) is Element of the carrier of L
v1 . v2 is set
Indices (1. (L,p)) is set
dom (1. (L,p)) is Element of K6(NAT)
width (1. (L,p)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width (1. (L,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 <= width (1. (L,p)) ) } is set
K7((dom (1. (L,p))),(Seg (width (1. (L,p))))) is set
[:(Seg p),(Seg p):] 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
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
v1 /. v2 is Element of the carrier of L
v2 - 1 is V11() V12() integer ext-real set
(m - x) * (v2 - 1) is V11() V12() integer ext-real set
(L,q,((m - x) * (v2 - 1))) is Element of the carrier of L
[m,m] is V26() set
Sum v1 is Element of the carrier of L
(L,p) * (1. L) is Element of the carrier of L
[m,x] is V26() set
0. L is V48(L) Element of the carrier of L
(L,p) * (0. 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
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,p,q) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
q " is Element of the carrier of L
(L,p,(q ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
(L,p,q) * (L,p,(q ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,p,(q ")) * (L,p,q) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
0. L is V48(L) Element of the carrier of L
(q ") " is Element of the carrier of L
(L,p,((q ") ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
(L,p,(q ")) * (L,p,((q ") ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
1. (L,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of p,p, the carrier of L
(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
(L,p) * (1. (L,p)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence 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
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 V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(q,L,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of q,1, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
m is Element of the carrier of L
(q,L,p,m) 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,q,m) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of q,q, the carrier of L
(L,q,m) * (q,L,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
Col ((q,L,p),1) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (len (q,L,p)) -tuples_on the carrier of L
len (q,L,p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(len (q,L,p)) -tuples_on the carrier of L is FinSequenceSet of the carrier of L
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(Col ((q,L,p),1)) . (v1 + 1) is set
p . v1 is Element of the carrier of L
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
dom (q,L,p) is Element of K6(NAT)
(q,L,p) * ((v1 + 1),1) is Element of the carrier of L
width (L,q,m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((L,q,m) * (q,L,p)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (L,q,m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width ((L,q,m) * (q,L,p)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width (q,L,p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Indices ((L,q,m) * (q,L,p)) is set
dom ((L,q,m) * (q,L,p)) is Element of K6(NAT)
Seg (width ((L,q,m) * (q,L,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 <= width ((L,q,m) * (q,L,p)) ) } is set
K7((dom ((L,q,m) * (q,L,p))),(Seg (width ((L,q,m) * (q,L,p))))) 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 q),(Seg (width ((L,q,m) * (q,L,p)))):] 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
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(q,L,p,m) . v1 is Element of the carrier of L
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
((L,q,m) * (q,L,p)) * ((v1 + 1),1) is Element of the carrier of L
Line ((L,q,m),(v1 + 1)) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like Element of (width (L,q,m)) -tuples_on the carrier of L
(width (L,q,m)) -tuples_on the carrier of L is FinSequenceSet of the carrier of L
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(Line ((L,q,m),(v1 + 1))) . (v2 + 1) is set
(L,q,m) * ((v1 + 1),(v2 + 1)) is Element of the carrier of L
Seg (width (L,q,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 <= width (L,q,m) ) } is set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(Line ((L,q,m),(v1 + 1))) . (v2 + 1) is set
v1 * v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,m,(v1 * v2)) is Element of the carrier of L
(L,q,m) * ((v1 + 1),(v2 + 1)) is Element of the carrier of L
(v1 + 1) - 1 is V11() V12() integer ext-real set
(v2 + 1) - 1 is V11() V12() integer ext-real set
((v1 + 1) - 1) * ((v2 + 1) - 1) is V11() V12() integer ext-real set
(L,m,(((v1 + 1) - 1) * ((v2 + 1) - 1))) is Element of the carrier of L
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
v2 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(Line ((L,q,m),(v1 + 1))) . (v2 + 1) is set
(Col ((q,L,p),1)) . (v2 + 1) is set
p . v2 is Element of the carrier of L
v1 * v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,m,(v1 * v2)) is Element of the carrier of L
u9 is Element of the carrier of L
u is Element of the carrier of L
k is Element of the carrier of L
u9 * u is Element of the carrier of L
(L,m,(v1 * v2)) * k is Element of the carrier of L
mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1))) is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence 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
m |^ v1 is Element of the carrier of L
(power L) . (m,v1) is set
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) . v2 is set
v2 -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
p . (v2 -' 1) is Element of the carrier of L
(power L) . ((m |^ v1),(v2 -' 1)) is Element of the carrier of L
(p . (v2 -' 1)) * ((power L) . ((m |^ v1),(v2 -' 1))) is Element of the carrier of L
dom (q,L,p) is Element of K6(NAT)
(Col ((q,L,p),1)) . v2 is set
(q,L,p) * (v2,1) is Element of the carrier of L
dom p is set
v2 - 1 is V11() V12() integer ext-real set
p . (v2 - 1) is set
p /. (v2 - 1) is Element of the carrier of L
Seg (width (L,q,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 <= width (L,q,m) ) } is set
(Line ((L,q,m),(v1 + 1))) . v2 is set
(L,q,m) * ((v1 + 1),v2) is Element of the carrier of L
len (Line ((L,q,m),(v1 + 1))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (Col ((q,L,p),1)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom (mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) is Element of K6(NAT)
u9 is Element of the carrier of L
u is Element of the carrier of L
u9 * u is Element of the carrier of L
v1 * (v2 - 1) is V11() V12() integer ext-real set
(L,m,(v1 * (v2 - 1))) is Element of the carrier of L
k is Element of the carrier of L
(L,m,(v1 * (v2 - 1))) * k is Element of the carrier of L
q - 1 is V11() V12() integer ext-real set
(q - 1) + 1 is V11() V12() integer ext-real set
l is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
l + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
(Line ((L,q,m),(v1 + 1))) . (l + 1) is set
l is Element of the carrier of L
(L,(m |^ v1),(v2 - 1)) is Element of the carrier of L
(power L) . ((m |^ v1),(v2 - 1)) is set
Sum (mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) is Element of the carrier of L
eval (p,(m |^ v1)) is Element of the carrier of L
0. L is V48(L) Element of the carrier of L
1 + (len p) is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
(mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) . v2 is set
v2 - 1 is V11() V12() integer ext-real set
(v2 - 1) + 1 is V11() V12() integer ext-real set
(len p) + 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
v2 -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
p . (v2 -' 1) is Element of the carrier of L
(power L) . ((m |^ v1),(v2 -' 1)) is Element of the carrier of L
(p . (v2 -' 1)) * ((power L) . ((m |^ v1),(v2 -' 1))) is Element of the carrier of L
(0. L) * ((power L) . ((m |^ v1),(v2 -' 1))) is Element of the carrier of L
len (Line ((L,q,m),(v1 + 1))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (Col ((q,L,p),1)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(len p) - (len p) is V11() V12() integer ext-real set
q - (len p) is V11() V12() integer ext-real set
u9 is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
Sum u9 is Element of the carrier of L
len u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom u9 is Element of K6(NAT)
v2 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg 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 <= v2 ) } is set
u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
u is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom u is Element of K6(NAT)
u is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom u is Element of K6(NAT)
u is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom u is Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
u . k is set
len u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(len u9) + (len u) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
u9 ^ u is Relation-like NAT -defined the carrier of L -valued Function-like FinSequence-like FinSequence of the carrier of L
dom (u9 ^ u) is Element of K6(NAT)
dom (mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) is Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
u9 . k is set
(mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) . k is set
Seg (len 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 <= len p ) } is set
k -' 1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
p . (k -' 1) is Element of the carrier of L
(power L) . ((m |^ v1),(k -' 1)) is Element of the carrier of L
(p . (k -' 1)) * ((power L) . ((m |^ v1),(k -' 1))) is Element of the carrier of L
k is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
(mlt ((Line ((L,q,m),(v1 + 1))),(Col ((q,L,p),1)))) . k is set
(u9 ^ u) . k is set
u9 . k is set
(len u9) + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
((len u9) + 1) - (len u9) is V11() V12() integer ext-real set
k - (len u9) is V11() V12() integer ext-real set
(len p) - q is V11() V12() integer ext-real set
q - q is V11() V12() integer ext-real set
- ((len p) - q) 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
lengthG is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (u9 ^ u) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
u . (k - (len u9)) is set
Sum u is Element of the carrier of L
(Sum u9) + (Sum u) is Element of the carrier of L
(Sum u9) + (0. L) is Element of the carrier of L
(Line ((L,q,m),(v1 + 1))) "*" (Col ((q,L,p),1)) is Element of the carrier of L
[(v1 + 1),1] is V26() set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(q,L,p,m) . v1 is Element of the carrier of L
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
((L,q,m) * (q,L,p)) * ((v1 + 1),1) 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
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 V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
(q,L,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of q,1, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
m is Element of the carrier of L
(q,L,p,m) 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,q,m) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of q,q, the carrier of L
(L,q,m) * (q,L,p) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,((L,q,m) * (q,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))
x is set
dom (q,L,p,m) is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width (L,q,m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (q,L,p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((L,q,m) * (q,L,p)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (L,q,m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(q,L,p,m) . x is set
v1 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
((L,q,m) * (q,L,p)) * ((v1 + 1),1) is Element of the carrier of L
(L,((L,q,m) * (q,L,p))) . x is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width (L,q,m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (q,L,p) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((L,q,m) * (q,L,p)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (L,q,m) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(q,L,p,m) . x is set
0. L is V48(L) Element of the carrier of L
(L,((L,q,m) * (q,L,p))) . x is set
v1 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom (L,((L,q,m) * (q,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 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
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))
m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
2 * m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,(2 * m)) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(2 * m) * (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(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) . ((2 * m),(1. L)) is Element of the carrier of L
(L,(2 * m)) * (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))
x is Element of the carrier of L
((2 * m),L,(p *' q),x) 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))
x " is Element of the carrier of L
((2 * m),L,((2 * m),L,(p *' q),x),(x ")) 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))
0_. L 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))
0. L is V48(L) Element of the carrier of L
K391( the carrier of L,NAT,(0. L)) is V8() 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))
((2 * m),L,(0_. L),(x ")) 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))
0_. L 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))
0. L is V48(L) Element of the carrier of L
K391( the carrier of L,NAT,(0. L)) is V8() 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))
((2 * m),L,(0_. L),(x ")) 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,(2 * m),x) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of 2 * m,2 * m, the carrier of L
the carrier of L * is FinSequenceSet of the carrier of L
(L,(2 * m),(x ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of 2 * m,2 * m, the carrier of L
(len p) + (len q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
m + m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (p *' q) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
((2 * m),L,(p *' q)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of 2 * m,1, the carrier of L
(L,(2 * m),x) * ((2 * m),L,(p *' q)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
u9 + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
((L,(2 * m),x) * ((2 * m),L,(p *' q))) * ((u9 + 1),1) is Element of the carrier of L
((2 * m),L,(p *' q),x) . u9 is Element of the carrier of L
0. L is V48(L) Element of the carrier of L
u9 is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative set
((2 * m),L,(p *' q),x) . u9 is Element of the carrier of L
len ((2 * m),L,(p *' q),x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width (L,(2 * m),(x ")) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len (L,(2 * m),x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,(2 * m),(x ")) * (L,(2 * m),x) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,(2 * m),x) * (L,(2 * m),(x ")) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
1. (L,(2 * m)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of 2 * m,2 * m, the carrier of L
(L,(2 * m)) * (1. (L,(2 * m))) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
u9 is set
(L,(2 * m)) * ((2 * m),L,(p *' q)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,((L,(2 * m)) * ((2 * m),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))
dom (L,((L,(2 * m)) * ((2 * m),L,(p *' q)))) is set
u 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
u + 1 is non empty V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real positive non negative Element of NAT
Seg (2 * 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 <= 2 * m ) } is set
len ((2 * m),L,(p *' q)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom ((2 * m),L,(p *' q)) is Element of K6(NAT)
width ((2 * m),L,(p *' q)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
Seg (width ((2 * m),L,(p *' 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 <= width ((2 * m),L,(p *' q)) ) } is set
[(u + 1),1] is V26() set
Indices ((2 * m),L,(p *' q)) is set
K7((dom ((2 * m),L,(p *' q))),(Seg (width ((2 * m),L,(p *' q))))) is set
len ((L,(2 * m)) * ((2 * m),L,(p *' q))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,((L,(2 * m)) * ((2 * m),L,(p *' q)))) . u9 is set
((L,(2 * m)) * ((2 * m),L,(p *' q))) * ((u + 1),1) is Element of the carrier of L
((2 * m),L,(p *' q)) * ((u + 1),1) is Element of the carrier of L
(L,(2 * m)) * (((2 * m),L,(p *' q)) * ((u + 1),1)) is Element of the carrier of L
(p *' q) . u is Element of the carrier of L
(L,(2 * m)) * ((p *' q) . u) is Element of the carrier of L
((L,(2 * m)) * (p *' q)) . u9 is set
u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((L,(2 * m)) * ((2 * m),L,(p *' q))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((2 * m),L,(p *' q)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,((L,(2 * m)) * ((2 * m),L,(p *' q)))) . u9 is set
(L,(2 * m)) * (0. L) is Element of the carrier of L
(p *' q) . u is Element of the carrier of L
(L,(2 * m)) * ((p *' q) . u) is Element of the carrier of L
((L,(2 * m)) * (p *' q)) . u9 is set
u is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
dom ((L,(2 * m)) * (p *' q)) is set
len ((2 * m),L,(p *' q)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width (L,(2 * m),x) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
len ((L,(2 * m),x) * ((2 * m),L,(p *' q))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width ((L,(2 * m),x) * ((2 * m),L,(p *' q))) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
width ((2 * m),L,(p *' q)) is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
((2 * m),L,((2 * m),L,(p *' q),x)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular Matrix of 2 * m,1, the carrier of L
(L,(2 * m),(x ")) * ((2 * m),L,((2 * m),L,(p *' q),x)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,((L,(2 * m),(x ")) * ((2 * m),L,((2 * m),L,(p *' q),x)))) 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,(2 * m),(x ")) * ((L,(2 * m),x) * ((2 * m),L,(p *' q))) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,((L,(2 * m),(x ")) * ((L,(2 * m),x) * ((2 * m),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))
((L,(2 * m),(x ")) * (L,(2 * m),x)) * ((2 * m),L,(p *' q)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,(((L,(2 * m),(x ")) * (L,(2 * m),x)) * ((2 * m),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))
(1. (L,(2 * m))) * ((2 * m),L,(p *' q)) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,(2 * m)) * ((1. (L,(2 * m))) * ((2 * m),L,(p *' q))) is Relation-like NAT -defined the carrier of L * -valued Function-like FinSequence-like tabular FinSequence of the carrier of L *
(L,((L,(2 * m)) * ((1. (L,(2 * m))) * ((2 * m),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))
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
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 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))
m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
2 * m is V4() V5() V6() V10() V11() V12() integer V32() V37() ext-real non negative Element of NAT
(L,(2 * m)) is Element of the carrier of L
1. L is V48(L) Element of the carrier of L
(2 * m) * (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(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) . ((2 * m),(1. L)) is Element of the carrier of L
(L,(2 * m)) " is Element of the carrier of L
x is Element of the carrier of L
((2 * m),L,p,x) 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))
((2 * m),L,q,x) 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,((2 * m),L,p,x),((2 * m),L,q,x)) 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))
x " is Element of the carrier of L
((2 * m),L,(L,((2 * m),L,p,x),((2 * m),L,q,x)),(x ")) 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,(2 * m)) ") * ((2 * m),L,(L,((2 * m),L,p,x),((2 * m),L,q,x)),(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))
((2 * m),L,(p *' q),x) 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))
((2 * m),L,((2 * m),L,(p *' q),x),(x ")) 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,(2 * m)) ") * ((2 * m),L,((2 * m),L,(p *' q),x),(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))
(L,(2 * m)) * (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))
((L,(2 * m)) ") * ((L,(2 * m)) * (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))
((L,(2 * m)) ") * (L,(2 * m)) is Element of the carrier of L
(((L,(2 * m)) ") * (L,(2 * m))) * (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))
(1. 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))