:: MIDSP_3 semantic presentation

REAL is set
NAT is non empty V24() V25() V26() Element of K19(REAL)
K19(REAL) is set
NAT is non empty V24() V25() V26() set
K19(NAT) is set
K19(NAT) is set
{} is empty V24() V25() V26() V28() V29() V30() V31() ext-real non negative V49() set
1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
0 is empty V24() V25() V26() V28() V29() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) + m is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty set
W is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
len W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
a is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
len a is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
p is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
len p is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
a ^ p is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
pm is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
x is Element of RAS
<*x*> is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
pm ^ <*x*> is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
len pm is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(pm ^ <*x*>) ^ p is V1() V4( NAT ) V5(RAS) Function-like FinSequence-like FinSequence of RAS
(len pm) + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg m is Element of K19(NAT)
RAS is V24() V25() V26() V30() V31() ext-real non negative V49() set
1 + RAS is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
a is V24() V25() V26() V30() V31() ext-real non negative V49() set
(W + 1) + a is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
p is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(W + 1) + p is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty set
RAS is Element of m
<*RAS*> is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
W is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
W . n is set
len W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
a is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
a ^ <*RAS*> is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
len a is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(len a) + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
p is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
(a ^ <*RAS*>) ^ p is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
<*RAS*> ^ p is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
a ^ (<*RAS*> ^ p) is V1() V4( NAT ) V5(m) Function-like FinSequence-like FinSequence of m
x is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W . x is set
a . x is set
dom a is Element of K19(NAT)
len (a ^ <*RAS*>) is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg n is Element of K19(NAT)
dom (a ^ <*RAS*>) is Element of K19(NAT)
(a ^ <*RAS*>) . n is set
len p is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(len (a ^ <*RAS*>)) + (len p) is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
x is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W . x is set
x - n is V31() ext-real V49() set
p . (x - n) is set
2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(m + 1) + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg m is Element of K19(NAT)
RAS is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
{RAS} is non empty set
(Seg m) \ {RAS} is Element of K19(NAT)
RAS + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is non empty set
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
RAS is V1() V4( NAT ) V5(n) Function-like V42(m) FinSequence-like Element of m -tuples_on n
W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
a is Element of n
RAS +* (W,a) is V1() Function-like set
RAS +* (W,a) is V1() V4( NAT ) V5(n) Function-like FinSequence-like FinSequence of n
dom (RAS +* (W,a)) is Element of K19(NAT)
dom RAS is Element of K19(NAT)
len (RAS +* (W,a)) is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
len RAS is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg n is Element of K19(NAT)
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty set
n -tuples_on RAS is functional non empty FinSequence-membered FinSequenceSet of RAS
W is Element of RAS
a is V1() V4( NAT ) V5(RAS) Function-like V42(n) FinSequence-like Element of n -tuples_on RAS
(RAS,n,a,m,W) is V1() V4( NAT ) V5(RAS) Function-like V42(n) FinSequence-like Element of n -tuples_on RAS
(RAS,n,a,m,W) . m is set
dom a is Element of K19(NAT)
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
{m} is non empty set
RAS is non empty set
n -tuples_on RAS is functional non empty FinSequence-membered FinSequenceSet of RAS
W is Element of RAS
a is V1() V4( NAT ) V5(RAS) Function-like V42(n) FinSequence-like Element of n -tuples_on RAS
dom a is Element of K19(NAT)
(dom a) \ {m} is Element of K19(NAT)
(RAS,n,a,m,W) is V1() V4( NAT ) V5(RAS) Function-like V42(n) FinSequence-like Element of n -tuples_on RAS
p is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(RAS,n,a,m,W) . p is set
a . p is set
m is non empty set
K20(m,m) is set
K20(K20(m,m),m) is set
K19(K20(K20(m,m),m)) is set
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n -tuples_on m is functional non empty FinSequence-membered FinSequenceSet of m
K20((n -tuples_on m),m) is set
K19(K20((n -tuples_on m),m)) is set
RAS is V1() V4(K20(m,m)) V5(m) Function-like V18(K20(m,m),m) Element of K19(K20(K20(m,m),m))
W is V1() V4(n -tuples_on m) V5(m) Function-like V18(n -tuples_on m,m) Element of K19(K20((n -tuples_on m),m))
(n,m,RAS,W) is (n) (n)
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like MidStr
the carrier of m is non empty set
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
the MIDPOINT of m is V1() V4(K20( the carrier of m, the carrier of m)) V5( the carrier of m) Function-like V18(K20( the carrier of m, the carrier of m), the carrier of m) Element of K19(K20(K20( the carrier of m, the carrier of m), the carrier of m))
K20( the carrier of m, the carrier of m) is set
K20(K20( the carrier of m, the carrier of m), the carrier of m) is set
K19(K20(K20( the carrier of m, the carrier of m), the carrier of m)) is set
RAS is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
((n + 2), the carrier of m, the MIDPOINT of m,RAS) is non empty (n + 2) (n + 2)
the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) is non empty set
a is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
a @ a is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) is V1() V4(K20( the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS))) V5( the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)) Function-like V18(K20( the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)) Element of K19(K20(K20( the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)))
K20( the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)) is set
K20(K20( the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)) is set
K19(K20(K20( the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)), the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS))) is set
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (a,a) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
p is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
a @ p is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (a,p) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
p @ a is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (p,a) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
pm is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
x is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
pm @ x is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (pm,x) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
(a @ p) @ (pm @ x) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . ((a @ p),(pm @ x)) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
a @ pm is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (a,pm) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
p @ x is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (p,x) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
(a @ pm) @ (p @ x) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . ((a @ pm),(p @ x)) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
v is Element of the carrier of m
v @ v is Element of the carrier of m
the MIDPOINT of m . (v,v) is Element of the carrier of m
x9 is Element of the carrier of m
qq is Element of the carrier of m
qq @ v is Element of the carrier of m
the MIDPOINT of m . (qq,v) is Element of the carrier of m
i is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
c₁₆ is Element of the carrier of m
i is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
c₁₇ is Element of the carrier of m
i @ i is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (i,i) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
c₁₆ @ c₁₇ is Element of the carrier of m
the MIDPOINT of m . (c₁₆,c₁₇) is Element of the carrier of m
x9 @ v is Element of the carrier of m
the MIDPOINT of m . (x9,v) is Element of the carrier of m
v @ x9 is Element of the carrier of m
the MIDPOINT of m . (v,x9) is Element of the carrier of m
k is Element of the carrier of m
pp is Element of the carrier of m
k @ pp is Element of the carrier of m
the MIDPOINT of m . (k,pp) is Element of the carrier of m
(v @ x9) @ (k @ pp) is Element of the carrier of m
the MIDPOINT of m . ((v @ x9),(k @ pp)) is Element of the carrier of m
v @ k is Element of the carrier of m
the MIDPOINT of m . (v,k) is Element of the carrier of m
x9 @ pp is Element of the carrier of m
the MIDPOINT of m . (x9,pp) is Element of the carrier of m
(v @ k) @ (x9 @ pp) is Element of the carrier of m
the MIDPOINT of m . ((v @ k),(x9 @ pp)) is Element of the carrier of m
i is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
i @ a is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
the MIDPOINT of ((n + 2), the carrier of m, the MIDPOINT of m,RAS) . (i,a) is Element of the carrier of ((n + 2), the carrier of m, the MIDPOINT of m,RAS)
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the non empty set is non empty set
K20( the non empty set , the non empty set ) is set
K20(K20( the non empty set , the non empty set ), the non empty set ) is set
K19(K20(K20( the non empty set , the non empty set ), the non empty set )) is set
the V1() V4(K20( the non empty set , the non empty set )) V5( the non empty set ) Function-like V18(K20( the non empty set , the non empty set ), the non empty set ) Element of K19(K20(K20( the non empty set , the non empty set ), the non empty set )) is V1() V4(K20( the non empty set , the non empty set )) V5( the non empty set ) Function-like V18(K20( the non empty set , the non empty set ), the non empty set ) Element of K19(K20(K20( the non empty set , the non empty set ), the non empty set ))
n -tuples_on the non empty set is functional non empty FinSequence-membered FinSequenceSet of the non empty set
K20((n -tuples_on the non empty set ), the non empty set ) is set
K19(K20((n -tuples_on the non empty set ), the non empty set )) is set
the V1() V4(n -tuples_on the non empty set ) V5( the non empty set ) Function-like V18(n -tuples_on the non empty set , the non empty set ) Element of K19(K20((n -tuples_on the non empty set ), the non empty set )) is V1() V4(n -tuples_on the non empty set ) V5( the non empty set ) Function-like V18(n -tuples_on the non empty set , the non empty set ) Element of K19(K20((n -tuples_on the non empty set ), the non empty set ))
(n, the non empty set , the V1() V4(K20( the non empty set , the non empty set )) V5( the non empty set ) Function-like V18(K20( the non empty set , the non empty set ), the non empty set ) Element of K19(K20(K20( the non empty set , the non empty set ), the non empty set )), the V1() V4(n -tuples_on the non empty set ) V5( the non empty set ) Function-like V18(n -tuples_on the non empty set , the non empty set ) Element of K19(K20((n -tuples_on the non empty set ), the non empty set ))) is non empty (n) (n)
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the non empty MidSp-like MidStr is non empty MidSp-like MidStr
the carrier of the non empty MidSp-like MidStr is non empty set
(n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr is functional non empty FinSequence-membered FinSequenceSet of the carrier of the non empty MidSp-like MidStr
K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ) is set
K19(K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr )) is set
the V1() V4((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ) V5( the carrier of the non empty MidSp-like MidStr ) Function-like V18((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ) Element of K19(K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr )) is V1() V4((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ) V5( the carrier of the non empty MidSp-like MidStr ) Function-like V18((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ) Element of K19(K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ))
the MIDPOINT of the non empty MidSp-like MidStr is V1() V4(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr )) V5( the carrier of the non empty MidSp-like MidStr ) Function-like V18(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ) Element of K19(K20(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ))
K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ) is set
K20(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ) is set
K19(K20(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr )) is set
((n + 2), the carrier of the non empty MidSp-like MidStr , the MIDPOINT of the non empty MidSp-like MidStr , the V1() V4((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ) V5( the carrier of the non empty MidSp-like MidStr ) Function-like V18((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ) Element of K19(K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ))) is non empty (n + 2) (n + 2)
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
RAS is Element of the carrier of m
<*RAS*> is set
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
RAS is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
W -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
a is V1() V4( NAT ) V5( the carrier of m) Function-like V42(RAS) FinSequence-like Element of RAS -tuples_on the carrier of m
p is V1() V4( NAT ) V5( the carrier of m) Function-like V42(W) FinSequence-like Element of W -tuples_on the carrier of m
a ^ p is V1() Function-like FinSequence-like set
RAS + W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(RAS + W) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
pm is V1() V4( NAT ) V5( the carrier of m) Function-like V42(RAS) FinSequence-like FinSequence of the carrier of m
x is V1() V4( NAT ) V5( the carrier of m) Function-like V42(W) FinSequence-like FinSequence of the carrier of m
pm ^ x is V1() V4( NAT ) V5( the carrier of m) Function-like FinSequence-like FinSequence of the carrier of m
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
RAS is Element of the carrier of m
(n,m,RAS) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
W is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,RAS),W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),W) is set
a is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 2) FinSequence-like Element of (n + 2) -tuples_on the carrier of m
the of m . a is Element of the carrier of m
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty MidSp-like (m + 2)
the carrier of RAS is non empty set
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(m + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg (m + 1) is Element of K19(NAT)
a is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(m + 1) FinSequence-like Element of (m + 1) -tuples_on the carrier of RAS
W is Element of the carrier of RAS
( the carrier of RAS,(m + 1),a,n,W) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(m + 1) FinSequence-like Element of (m + 1) -tuples_on the carrier of RAS
( the carrier of RAS,(m + 1),a,n,W) . n is set
p is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
dom a is Element of K19(NAT)
{n} is non empty set
(dom a) \ {n} is Element of K19(NAT)
( the carrier of RAS,(m + 1),a,n,W) . p is set
a . p is set
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg (m + 1) is Element of K19(NAT)
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
W is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
Seg (n + 1) is Element of K19(NAT)
a is V24() V25() V26() V30() V31() ext-real non negative V49() set
RAS . a is set
W . a is set
p is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS . p is set
W . p is set
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty MidSp-like (n + 2)
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
W is Element of the carrier of RAS
a is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
( the carrier of RAS,(n + 1),a,m,W) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
p is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
( the carrier of RAS,(n + 1),a,m,W) . p is set
Seg (n + 1) is Element of K19(NAT)
m is non empty set
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on m is functional non empty FinSequence-membered FinSequenceSet of m
RAS is V1() V4( NAT ) V5(m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on m
W is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS . W is set
Seg (n + 1) is Element of K19(NAT)
a is non empty set
len RAS is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
dom RAS is Element of K19(NAT)
rng RAS is set
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
W is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
a is Element of the carrier of m
RAS +* (W,a) is V1() Function-like set
( the carrier of m,(n + 1),RAS,W,a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
W is Element of the carrier of m
a is Element of the carrier of m
W @ a is Element of the carrier of m
the MIDPOINT of m is V1() V4(K20( the carrier of m, the carrier of m)) V5( the carrier of m) Function-like V18(K20( the carrier of m, the carrier of m), the carrier of m) Element of K19(K20(K20( the carrier of m, the carrier of m), the carrier of m))
K20( the carrier of m, the carrier of m) is set
K20(K20( the carrier of m, the carrier of m), the carrier of m) is set
K19(K20(K20( the carrier of m, the carrier of m), the carrier of m)) is set
the MIDPOINT of m . (W,a) is Element of the carrier of m
p is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,p,RAS,a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,p,RAS,(W @ a)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,W,(n,m,p,RAS,(W @ a))) is Element of the carrier of m
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,W),(n,m,p,RAS,(W @ a))) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),(n,m,p,RAS,(W @ a))) is set
pm is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,W,pm) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,W),pm) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),pm) is set
W @ (n,m,W,pm) is Element of the carrier of m
the MIDPOINT of m . (W,(n,m,W,pm)) is Element of the carrier of m
(n,m,pm,RAS,(W @ a)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
x9 is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of m,(n,m,pm,RAS,(W @ a)),x9) is Element of the carrier of m
(n, the carrier of m,(n,m,p,RAS,(W @ a)),x9) is Element of the carrier of m
(n, the carrier of m,(n,m,p,RAS,(W @ a)),RAS) is Element of the carrier of m
(n, the carrier of m,pm,x9) is Element of the carrier of m
(n, the carrier of m,p,x9) is Element of the carrier of m
(n, the carrier of m,pm,RAS) is Element of the carrier of m
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty MidSp-like (m + 2)
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(m + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg (m + 1) is Element of K19(NAT)
p is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(m + 1) FinSequence-like Element of (m + 1) -tuples_on the carrier of the algebra of W
a is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(m + 1),p,n,a) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(m + 1) FinSequence-like Element of (m + 1) -tuples_on the carrier of the algebra of W
( the carrier of the algebra of W,(m + 1),p,n,a) . n is set
pm is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
dom p is Element of K19(NAT)
{n} is non empty set
(dom p) \ {n} is Element of K19(NAT)
( the carrier of the algebra of W,(m + 1),p,n,a) . pm is set
p . pm is set
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty MidSp-like (n + 2)
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
(n + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
a is Element of the carrier of the algebra of W
p is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),p,m,a) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
pm is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,a),pm) is Element of the carrier of the algebra of W
Seg (n + 1) is Element of K19(NAT)
pm is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
( the carrier of the algebra of W,(n + 1),p,x,a) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,x,a),pm) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,p,pm) is Element of the carrier of the algebra of W
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
RAS is ATLAS-like AtlasStr over m
the algebra of RAS is non empty L7()
the carrier of the algebra of RAS is non empty set
(n + 1) -tuples_on the carrier of the algebra of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of RAS
W is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
a is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
Seg (n + 1) is Element of K19(NAT)
p is V24() V25() V26() V30() V31() ext-real non negative V49() set
W . p is set
a . p is set
pm is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of RAS,W,pm) is Element of the carrier of the algebra of RAS
(n, the carrier of the algebra of RAS,a,pm) is Element of the carrier of the algebra of RAS
F₂() is non empty set
F₁() is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
F₁() + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg (F₁() + 1) is Element of K19(NAT)
m is V1() V4( NAT ) V5(F₂()) Function-like FinSequence-like FinSequence of F₂()
len m is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
dom m is Element of K19(NAT)
RAS is V24() V25() V26() V30() V31() ext-real non negative V49() (F₁())
m . RAS is set
F₃(RAS) is Element of F₂()
n is non empty set
RAS is V24() V25() V26() V30() V31() ext-real non negative V49() (F₁())
m . RAS is set
F₃(RAS) is Element of F₂()
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
RAS is ATLAS-like AtlasStr over m
the algebra of RAS is non empty L7()
the carrier of the algebra of RAS is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of the algebra of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of RAS
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
W is Element of the carrier of m
a is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
p is V1() V4( NAT ) V5( the carrier of m) Function-like FinSequence-like FinSequence of the carrier of m
len p is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
pm is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of m,pm,x) is Element of the carrier of m
(n, the carrier of the algebra of RAS,a,x) is Element of the carrier of the algebra of RAS
(W,(n, the carrier of the algebra of RAS,a,x)) . RAS is Element of the carrier of m
p is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
pm is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of m,p,x) is Element of the carrier of m
(n, the carrier of m,pm,x) is Element of the carrier of m
(n, the carrier of the algebra of RAS,a,x) is Element of the carrier of the algebra of RAS
(W,(n, the carrier of the algebra of RAS,a,x)) . RAS is Element of the carrier of m
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is ATLAS-like AtlasStr over m
the algebra of RAS is non empty L7()
the carrier of the algebra of RAS is non empty set
(n + 1) -tuples_on the carrier of the algebra of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of RAS
W is Element of the carrier of m
a is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
p is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like FinSequence-like FinSequence of the carrier of the algebra of RAS
len p is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
pm is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of RAS,pm,x) is Element of the carrier of the algebra of RAS
(n, the carrier of m,a,x) is Element of the carrier of m
RAS . (W,(n, the carrier of m,a,x)) is Element of the carrier of the algebra of RAS
p is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
pm is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of RAS,p,x) is Element of the carrier of the algebra of RAS
(n, the carrier of the algebra of RAS,pm,x) is Element of the carrier of the algebra of RAS
(n, the carrier of m,a,x) is Element of the carrier of m
RAS . (W,(n, the carrier of m,a,x)) is Element of the carrier of the algebra of RAS
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is Element of the carrier of m
W is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
a is ATLAS-like AtlasStr over m
the algebra of a is non empty L7()
the carrier of the algebra of a is non empty set
(n + 1) -tuples_on the carrier of the algebra of a is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of a
(n,m,a,RAS,W) is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
p is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
(n,m,a,RAS,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
pm is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of m,W,pm) is Element of the carrier of m
a . (RAS,(n, the carrier of m,W,pm)) is Element of the carrier of the algebra of a
(n, the carrier of the algebra of a,p,pm) is Element of the carrier of the algebra of a
(RAS,(n, the carrier of the algebra of a,p,pm)) . a is Element of the carrier of m
pm is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of a,p,pm) is Element of the carrier of the algebra of a
(RAS,(n, the carrier of the algebra of a,p,pm)) . a is Element of the carrier of m
(n, the carrier of m,W,pm) is Element of the carrier of m
a . (RAS,(n, the carrier of m,W,pm)) is Element of the carrier of the algebra of a
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
W is ATLAS-like AtlasStr over m
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
RAS is Element of the carrier of m
a is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,m,W,RAS,a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,W,RAS,(n,m,W,RAS,a)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
a is ATLAS-like AtlasStr over m
RAS is Element of the carrier of m
W is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,a,RAS,W) is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
the algebra of a is non empty L7()
the carrier of the algebra of a is non empty set
(n + 1) -tuples_on the carrier of the algebra of a is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of a
(n,m,a,RAS,(n,m,a,RAS,W)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
RAS is ATLAS-like AtlasStr over m
the algebra of RAS is non empty L7()
the carrier of the algebra of RAS is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of the algebra of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of RAS
W is Element of the carrier of m
a is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
(n,m,RAS,W,a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,W,(n,m,RAS,W,a)) is Element of the carrier of m
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,a)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,a)) is set
RAS . (W,(n,m,W,(n,m,RAS,W,a))) is Element of the carrier of the algebra of RAS
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is Element of the carrier of m
W is Element of the carrier of m
a is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,a) is Element of the carrier of m
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,RAS) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),a) is set
p is ATLAS-like AtlasStr over m
the algebra of p is non empty L7()
the carrier of the algebra of p is non empty set
(n + 1) -tuples_on the carrier of the algebra of p is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of p
(n,m,p,RAS,a) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
p . (RAS,W) is Element of the carrier of the algebra of p
pm is Element of the carrier of the algebra of p
x is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n,m,p,RAS,x) is Element of the carrier of the algebra of p
(n,m,p,RAS,x) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,(n,m,p,RAS,x)) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),(n,m,p,RAS,x)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),(n,m,p,RAS,x)) is set
p . (RAS,(n,m,RAS,(n,m,p,RAS,x))) is Element of the carrier of the algebra of p
p . (RAS,(n,m,RAS,a)) is Element of the carrier of the algebra of p
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n + 2)
the carrier of m is non empty set
RAS is ATLAS-like AtlasStr over m
the algebra of RAS is non empty L7()
the carrier of the algebra of RAS is non empty set
(n + 1) -tuples_on the carrier of the algebra of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of RAS
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
W is Element of the carrier of m
a is Element of the carrier of m
p is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,W,p) is Element of the carrier of m
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,W),p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),p) is set
a @ (n,m,W,p) is Element of the carrier of m
the MIDPOINT of m is V1() V4(K20( the carrier of m, the carrier of m)) V5( the carrier of m) Function-like V18(K20( the carrier of m, the carrier of m), the carrier of m) Element of K19(K20(K20( the carrier of m, the carrier of m), the carrier of m))
K20( the carrier of m, the carrier of m) is set
K20(K20( the carrier of m, the carrier of m), the carrier of m) is set
K19(K20(K20( the carrier of m, the carrier of m), the carrier of m)) is set
the MIDPOINT of m . (a,(n,m,W,p)) is Element of the carrier of m
pm is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,a,pm) is Element of the carrier of m
(n,m,a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,a),pm) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,a),pm) is set
W @ (n,m,a,pm) is Element of the carrier of m
the MIDPOINT of m . (W,(n,m,a,pm)) is Element of the carrier of m
(n,m,RAS,W,p) is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
(n,m,RAS,W,(n,m,RAS,W,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,W,(n,m,RAS,W,(n,m,RAS,W,p))) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,(n,m,RAS,W,p))) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,(n,m,RAS,W,p))) is set
RAS . (W,(n,m,W,(n,m,RAS,W,(n,m,RAS,W,p)))) is Element of the carrier of the algebra of RAS
(n,m,RAS,W,(n,m,RAS,W,p)) is Element of the carrier of the algebra of RAS
(n,m,RAS,a,(n,m,RAS,W,p)) is Element of the carrier of the algebra of RAS
(n,m,RAS,a,(n,m,RAS,W,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,a,(n,m,RAS,a,(n,m,RAS,W,p))) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,(n,m,RAS,W,p))) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,(n,m,RAS,W,p))) is set
RAS . (a,(n,m,a,(n,m,RAS,a,(n,m,RAS,W,p)))) is Element of the carrier of the algebra of RAS
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of m,pm,x) is Element of the carrier of m
W @ (n, the carrier of m,pm,x) is Element of the carrier of m
the MIDPOINT of m . (W,(n, the carrier of m,pm,x)) is Element of the carrier of m
(n, the carrier of m,p,x) is Element of the carrier of m
a @ (n, the carrier of m,p,x) is Element of the carrier of m
the MIDPOINT of m . (a,(n, the carrier of m,p,x)) is Element of the carrier of m
RAS . (W,(n, the carrier of m,p,x)) is Element of the carrier of the algebra of RAS
RAS . (a,(n, the carrier of m,pm,x)) is Element of the carrier of the algebra of RAS
(n, the carrier of the algebra of RAS,(n,m,RAS,W,p),x) is Element of the carrier of the algebra of RAS
(n,m,RAS,a,pm) is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
(n, the carrier of the algebra of RAS,(n,m,RAS,a,pm),x) is Element of the carrier of the algebra of RAS
RAS . (W,(n,m,W,p)) is Element of the carrier of the algebra of RAS
(n,m,RAS,a,(n,m,RAS,a,pm)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,a,(n,m,RAS,a,(n,m,RAS,a,pm))) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,(n,m,RAS,a,pm))) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,(n,m,RAS,a,pm))) is set
RAS . (a,(n,m,a,(n,m,RAS,a,(n,m,RAS,a,pm)))) is Element of the carrier of the algebra of RAS
RAS . (a,(n,m,a,pm)) is Element of the carrier of the algebra of RAS
W is Element of the carrier of m
p is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
(n,m,RAS,W,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
a is Element of the carrier of m
(n,m,RAS,a,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,W,(n,m,RAS,W,p)) is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
(n,m,RAS,a,(n,m,RAS,a,p)) is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
v is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of m,(n,m,RAS,W,p),v) is Element of the carrier of m
RAS . (W,(n, the carrier of m,(n,m,RAS,W,p),v)) is Element of the carrier of the algebra of RAS
(n, the carrier of the algebra of RAS,(n,m,RAS,W,(n,m,RAS,W,p)),v) is Element of the carrier of the algebra of RAS
(n, the carrier of m,(n,m,RAS,a,p),v) is Element of the carrier of m
RAS . (a,(n, the carrier of m,(n,m,RAS,a,p),v)) is Element of the carrier of the algebra of RAS
W @ (n, the carrier of m,(n,m,RAS,a,p),v) is Element of the carrier of m
the MIDPOINT of m is V1() V4(K20( the carrier of m, the carrier of m)) V5( the carrier of m) Function-like V18(K20( the carrier of m, the carrier of m), the carrier of m) Element of K19(K20(K20( the carrier of m, the carrier of m), the carrier of m))
K20( the carrier of m, the carrier of m) is set
K20(K20( the carrier of m, the carrier of m), the carrier of m) is set
K19(K20(K20( the carrier of m, the carrier of m), the carrier of m)) is set
the MIDPOINT of m . (W,(n, the carrier of m,(n,m,RAS,a,p),v)) is Element of the carrier of m
a @ (n, the carrier of m,(n,m,RAS,W,p),v) is Element of the carrier of m
the MIDPOINT of m . (a,(n, the carrier of m,(n,m,RAS,W,p),v)) is Element of the carrier of m
(n,m,a,(n,m,RAS,a,p)) is Element of the carrier of m
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,p)) is set
W @ (n,m,a,(n,m,RAS,a,p)) is Element of the carrier of m
the MIDPOINT of m . (W,(n,m,a,(n,m,RAS,a,p))) is Element of the carrier of m
(n,m,W,(n,m,RAS,W,p)) is Element of the carrier of m
(n,m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,p)) is set
a @ (n,m,W,(n,m,RAS,W,p)) is Element of the carrier of m
the MIDPOINT of m . (a,(n,m,W,(n,m,RAS,W,p))) is Element of the carrier of m
(n,m,RAS,W,p) is Element of the carrier of the algebra of RAS
RAS . (W,(n,m,W,(n,m,RAS,W,p))) is Element of the carrier of the algebra of RAS
(n,m,RAS,a,p) is Element of the carrier of the algebra of RAS
RAS . (a,(n,m,a,(n,m,RAS,a,p))) is Element of the carrier of the algebra of RAS
W is Element of the carrier of m
p is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
(n,m,RAS,W,p) is Element of the carrier of the algebra of RAS
(n,m,RAS,W,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,W,(n,m,RAS,W,p)) is Element of the carrier of m
(n,m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),(n,m,RAS,W,p)) is set
RAS . (W,(n,m,W,(n,m,RAS,W,p))) is Element of the carrier of the algebra of RAS
a is Element of the carrier of m
(n,m,RAS,a,p) is Element of the carrier of the algebra of RAS
(n,m,RAS,a,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,a,(n,m,RAS,a,p)) is Element of the carrier of m
(n,m,a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,a),(n,m,RAS,a,p)) is set
RAS . (a,(n,m,a,(n,m,RAS,a,p))) is Element of the carrier of the algebra of RAS
pm is Element of the carrier of m
v is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
(n,m,RAS,pm,v) is Element of the carrier of the algebra of RAS
(n,m,RAS,pm,v) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,pm,(n,m,RAS,pm,v)) is Element of the carrier of m
(n,m,pm) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,pm),(n,m,RAS,pm,v)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,pm),(n,m,RAS,pm,v)) is set
RAS . (pm,(n,m,pm,(n,m,RAS,pm,v))) is Element of the carrier of the algebra of RAS
x is Element of the carrier of m
(n,m,RAS,x,v) is Element of the carrier of the algebra of RAS
(n,m,RAS,x,v) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,x,(n,m,RAS,x,v)) is Element of the carrier of m
(n,m,x) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,x),(n,m,RAS,x,v)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,x),(n,m,RAS,x,v)) is set
RAS . (x,(n,m,x,(n,m,RAS,x,v))) is Element of the carrier of the algebra of RAS
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg (n + 1) is Element of K19(NAT)
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
Seg (n + 1) is Element of K19(NAT)
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the non empty MidSp-like MidStr is non empty MidSp-like MidStr
the carrier of the non empty MidSp-like MidStr is non empty set
(n + 1) + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
((n + 1) + 1) -tuples_on the carrier of the non empty MidSp-like MidStr is functional non empty FinSequence-membered FinSequenceSet of the carrier of the non empty MidSp-like MidStr
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n + 1)
K20((((n + 1) + 1) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ) is set
K19(K20((((n + 1) + 1) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr )) is set
pm is V1() V4(((n + 1) + 1) -tuples_on the carrier of the non empty MidSp-like MidStr ) V5( the carrier of the non empty MidSp-like MidStr ) Function-like V18(((n + 1) + 1) -tuples_on the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ) Element of K19(K20((((n + 1) + 1) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ))
(n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr is functional non empty FinSequence-membered FinSequenceSet of the carrier of the non empty MidSp-like MidStr
K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ) is set
K19(K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr )) is set
the MIDPOINT of the non empty MidSp-like MidStr is V1() V4(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr )) V5( the carrier of the non empty MidSp-like MidStr ) Function-like V18(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ) Element of K19(K20(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ))
K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ) is set
K20(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ) is set
K19(K20(K20( the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr )) is set
x is V1() V4((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ) V5( the carrier of the non empty MidSp-like MidStr ) Function-like V18((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr , the carrier of the non empty MidSp-like MidStr ) Element of K19(K20(((n + 2) -tuples_on the carrier of the non empty MidSp-like MidStr ), the carrier of the non empty MidSp-like MidStr ))
((n + 2), the carrier of the non empty MidSp-like MidStr , the MIDPOINT of the non empty MidSp-like MidStr ,x) is non empty (n + 2) (n + 2)
v is non empty MidSp-like (n + 2)
the carrier of v is non empty set
(n + 1) -tuples_on the carrier of v is functional non empty FinSequence-membered FinSequenceSet of the carrier of v
x9 is Element of the carrier of v
k is Element of the carrier of v
qq is V1() V4( NAT ) V5( the carrier of v) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of v
pp is V1() V4( NAT ) V5( the carrier of v) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of v
(n,v,k,qq) is Element of the carrier of v
the of v is V1() V4((n + 2) -tuples_on the carrier of v) V5( the carrier of v) Function-like V18((n + 2) -tuples_on the carrier of v, the carrier of v) Element of K19(K20(((n + 2) -tuples_on the carrier of v), the carrier of v))
(n + 2) -tuples_on the carrier of v is functional non empty FinSequence-membered FinSequenceSet of the carrier of v
K20(((n + 2) -tuples_on the carrier of v), the carrier of v) is set
K19(K20(((n + 2) -tuples_on the carrier of v), the carrier of v)) is set
(n,v,k) is V1() V4( NAT ) V5( the carrier of v) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of v
1 -tuples_on the carrier of v is functional non empty FinSequence-membered FinSequenceSet of the carrier of v
(n,v,1,(n + 1),(n,v,k),qq) is V1() V4( NAT ) V5( the carrier of v) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of v
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of v is functional non empty FinSequence-membered FinSequenceSet of the carrier of v
the of v . (n,v,1,(n + 1),(n,v,k),qq) is set
x9 @ (n,v,k,qq) is Element of the carrier of v
the MIDPOINT of v is V1() V4(K20( the carrier of v, the carrier of v)) V5( the carrier of v) Function-like V18(K20( the carrier of v, the carrier of v), the carrier of v) Element of K19(K20(K20( the carrier of v, the carrier of v), the carrier of v))
K20( the carrier of v, the carrier of v) is set
K20(K20( the carrier of v, the carrier of v), the carrier of v) is set
K19(K20(K20( the carrier of v, the carrier of v), the carrier of v)) is set
the MIDPOINT of v . (x9,(n,v,k,qq)) is Element of the carrier of v
(n,v,x9,pp) is Element of the carrier of v
(n,v,x9) is V1() V4( NAT ) V5( the carrier of v) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of v
(n,v,1,(n + 1),(n,v,x9),pp) is V1() V4( NAT ) V5( the carrier of v) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of v
the of v . (n,v,1,(n + 1),(n,v,x9),pp) is set
k @ (n,v,x9,pp) is Element of the carrier of v
the MIDPOINT of v . (k,(n,v,x9,pp)) is Element of the carrier of v
(n,v,1,(n + 1),(n,v,x9),pp) . m is set
(n,v,1,(n + 1),(n,v,k),qq) . m is set
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n)
the carrier of m is non empty set
RAS is Element of the carrier of m
W is Element of the carrier of m
a is ATLAS-like AtlasStr over m
the algebra of a is non empty L7()
the carrier of the algebra of a is non empty set
(n + 1) -tuples_on the carrier of the algebra of a is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of a
p is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
(n,m,a,RAS,p) is Element of the carrier of the algebra of a
(n,m,a,RAS,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,RAS,(n,m,a,RAS,p)) is Element of the carrier of m
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,RAS) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),(n,m,a,RAS,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),(n,m,a,RAS,p)) is set
a . (RAS,(n,m,RAS,(n,m,a,RAS,p))) is Element of the carrier of the algebra of a
(n,m,a,W,p) is Element of the carrier of the algebra of a
(n,m,a,W,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,W,(n,m,a,W,p)) is Element of the carrier of m
(n,m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,W),(n,m,a,W,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,W),(n,m,a,W,p)) is set
a . (W,(n,m,W,(n,m,a,W,p))) is Element of the carrier of the algebra of a
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n)
RAS is ATLAS-like AtlasStr over m
the algebra of RAS is non empty L7()
the carrier of the algebra of RAS is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of the algebra of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of RAS
the carrier of m is non empty set
W is V1() V4( NAT ) V5( the carrier of the algebra of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of RAS
the Element of the carrier of m is Element of the carrier of m
(n,m,RAS, the Element of the carrier of m,W) is Element of the carrier of the algebra of RAS
(n,m,RAS, the Element of the carrier of m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m, the Element of the carrier of m,(n,m,RAS, the Element of the carrier of m,W)) is Element of the carrier of m
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m, the Element of the carrier of m) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m, the Element of the carrier of m),(n,m,RAS, the Element of the carrier of m,W)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m, the Element of the carrier of m),(n,m,RAS, the Element of the carrier of m,W)) is set
RAS . ( the Element of the carrier of m,(n,m, the Element of the carrier of m,(n,m,RAS, the Element of the carrier of m,W))) is Element of the carrier of the algebra of RAS
p is Element of the carrier of m
(n,m,RAS,p,W) is Element of the carrier of the algebra of RAS
(n,m,RAS,p,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,p,(n,m,RAS,p,W)) is Element of the carrier of m
(n,m,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
(n,m,1,(n + 1),(n,m,p),(n,m,RAS,p,W)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,p),(n,m,RAS,p,W)) is set
RAS . (p,(n,m,p,(n,m,RAS,p,W))) is Element of the carrier of the algebra of RAS
the Element of the carrier of m is Element of the carrier of m
p is Element of the carrier of the algebra of RAS
pm is Element of the carrier of the algebra of RAS
(n,m,RAS, the Element of the carrier of m,W) is Element of the carrier of the algebra of RAS
(n,m,RAS, the Element of the carrier of m,W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m, the Element of the carrier of m,(n,m,RAS, the Element of the carrier of m,W)) is Element of the carrier of m
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m, the Element of the carrier of m) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m, the Element of the carrier of m),(n,m,RAS, the Element of the carrier of m,W)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m, the Element of the carrier of m),(n,m,RAS, the Element of the carrier of m,W)) is set
RAS . ( the Element of the carrier of m,(n,m, the Element of the carrier of m,(n,m,RAS, the Element of the carrier of m,W))) is Element of the carrier of the algebra of RAS
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is Element of the carrier of m
W is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,W) is Element of the carrier of m
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,RAS) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),W) is set
a is ATLAS-like AtlasStr over m
the algebra of a is non empty L7()
the carrier of the algebra of a is non empty set
(n + 1) -tuples_on the carrier of the algebra of a is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of a
(n,m,a,RAS,W) is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
a . (RAS,(n,m,RAS,W)) is Element of the carrier of the algebra of a
p is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
(n,m,a,p) is Element of the carrier of the algebra of a
(n,m,a,RAS,p) is Element of the carrier of the algebra of a
(n,m,a,RAS,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,(n,m,a,RAS,p)) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),(n,m,a,RAS,p)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),(n,m,a,RAS,p)) is set
a . (RAS,(n,m,RAS,(n,m,a,RAS,p))) is Element of the carrier of the algebra of a
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is Element of the carrier of m
W is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,W) is Element of the carrier of m
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,RAS) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),W) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),W) is set
a is ATLAS-like AtlasStr over m
the algebra of a is non empty L7()
the carrier of the algebra of a is non empty set
(n + 1) -tuples_on the carrier of the algebra of a is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of a
a . (RAS,(n,m,RAS,W)) is Element of the carrier of the algebra of a
p is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
(n,m,a,RAS,p) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,a,p) is Element of the carrier of the algebra of a
(n,m,a,RAS,W) is V1() V4( NAT ) V5( the carrier of the algebra of a) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of a
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is Element of the carrier of m
W is Element of the carrier of m
a is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,a) is Element of the carrier of m
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,RAS) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),a) is set
p is ATLAS-like AtlasStr over m
the algebra of p is non empty L7()
the carrier of the algebra of p is non empty set
(n + 1) -tuples_on the carrier of the algebra of p is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of p
(n,m,p,RAS,a) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
p . (RAS,W) is Element of the carrier of the algebra of p
pm is Element of the carrier of the algebra of p
x is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n,m,p,x) is Element of the carrier of the algebra of p
(n,m,p,RAS,x) is Element of the carrier of the algebra of p
(n,m,p,RAS,x) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,(n,m,p,RAS,x)) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),(n,m,p,RAS,x)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),(n,m,p,RAS,x)) is set
p . (RAS,(n,m,RAS,(n,m,p,RAS,x))) is Element of the carrier of the algebra of p
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is non empty MidSp-like (n)
the carrier of m is non empty set
(n + 1) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
RAS is Element of the carrier of m
W is Element of the carrier of m
a is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,RAS,a) is Element of the carrier of m
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of m is V1() V4((n + 2) -tuples_on the carrier of m) V5( the carrier of m) Function-like V18((n + 2) -tuples_on the carrier of m, the carrier of m) Element of K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m))
(n + 2) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
K20(((n + 2) -tuples_on the carrier of m), the carrier of m) is set
K19(K20(((n + 2) -tuples_on the carrier of m), the carrier of m)) is set
(n,m,RAS) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of m
1 -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),a) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of m is functional non empty FinSequence-membered FinSequenceSet of the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),a) is set
p is ATLAS-like AtlasStr over m
the algebra of p is non empty L7()
the carrier of the algebra of p is non empty set
(n + 1) -tuples_on the carrier of the algebra of p is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of p
pm is Element of the carrier of the algebra of p
(RAS,pm) . p is Element of the carrier of m
x is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n,m,p,RAS,x) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of m
(n,m,p,x) is Element of the carrier of the algebra of p
(n,m,p,RAS,x) is Element of the carrier of the algebra of p
(n,m,RAS,(n,m,p,RAS,x)) is Element of the carrier of m
(n,m,1,(n + 1),(n,m,RAS),(n,m,p,RAS,x)) is V1() V4( NAT ) V5( the carrier of m) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of m
the of m . (n,m,1,(n + 1),(n,m,RAS),(n,m,p,RAS,x)) is set
p . (RAS,(n,m,RAS,(n,m,p,RAS,x))) is Element of the carrier of the algebra of p
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
W is Element of the carrier of RAS
a is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,p,m,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
pm is ATLAS-like AtlasStr over RAS
the algebra of pm is non empty L7()
the carrier of the algebra of pm is non empty set
(n + 1) -tuples_on the carrier of the algebra of pm is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of pm
(n,RAS,pm,W,p) is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
pm . (W,a) is Element of the carrier of the algebra of pm
(n,RAS,pm,W,(n,RAS,p,m,a)) is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
x is Element of the carrier of the algebra of pm
v is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
( the carrier of the algebra of pm,(n + 1),v,m,x) is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
qq is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of pm,(n,RAS,pm,W,(n,RAS,p,m,a)),qq) is Element of the carrier of the algebra of pm
(n, the carrier of the algebra of pm,( the carrier of the algebra of pm,(n + 1),v,m,x),qq) is Element of the carrier of the algebra of pm
(n, the carrier of RAS,(n,RAS,p,m,a),qq) is Element of the carrier of RAS
pm . (W,(n, the carrier of RAS,(n,RAS,p,m,a),qq)) is Element of the carrier of the algebra of pm
(n, the carrier of RAS,(n,RAS,p,m,a),qq) is Element of the carrier of RAS
pm . (W,(n, the carrier of RAS,(n,RAS,p,m,a),qq)) is Element of the carrier of the algebra of pm
(n, the carrier of RAS,p,qq) is Element of the carrier of RAS
pm . (W,(n, the carrier of RAS,p,qq)) is Element of the carrier of the algebra of pm
(n, the carrier of the algebra of pm,v,qq) is Element of the carrier of the algebra of pm
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
W is Element of the carrier of RAS
a is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,p,m,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
pm is ATLAS-like AtlasStr over RAS
the algebra of pm is non empty L7()
the carrier of the algebra of pm is non empty set
(n + 1) -tuples_on the carrier of the algebra of pm is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of pm
x is Element of the carrier of the algebra of pm
(W,x) . pm is Element of the carrier of RAS
v is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
(n,RAS,pm,W,v) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
( the carrier of the algebra of pm,(n + 1),v,m,x) is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
(n,RAS,pm,W,( the carrier of the algebra of pm,(n + 1),v,m,x)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,pm,W,p) is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
pm . (W,a) is Element of the carrier of the algebra of pm
(n,RAS,pm,W,(n,RAS,p,m,a)) is V1() V4( NAT ) V5( the carrier of the algebra of pm) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of pm
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
(n + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
0. W is Element of the carrier of the algebra of W
the carrier of RAS is non empty set
the Element of the carrier of RAS is Element of the carrier of RAS
( the Element of the carrier of RAS,(0. W)) . W is Element of the carrier of RAS
pm is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),pm,m,(0. W)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),pm,m,(0. W))) is Element of the carrier of the algebra of W
(n,RAS,W, the Element of the carrier of RAS,pm) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,(n,RAS,W, the Element of the carrier of RAS,pm),m, the Element of the carrier of RAS) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),pm,m,(0. W))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,pm),m, the Element of the carrier of RAS)) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS, the Element of the carrier of RAS) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,pm),m, the Element of the carrier of RAS)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,pm),m, the Element of the carrier of RAS)) is set
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
a is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,p,m,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,p,m,a)) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,p,m,a)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,p,m,a)) is set
W . (a,a) is Element of the carrier of the algebra of W
(n,RAS,W,a,p) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,p),m,(0. W)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,a,(n,RAS,p,m,a)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,p),m,(0. W))) is Element of the carrier of the algebra of W
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
(n + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
the carrier of RAS is non empty set
the Element of the carrier of RAS is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n, the carrier of the algebra of W,p,m) is Element of the carrier of the algebra of W
Double (n, the carrier of the algebra of W,p,m) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))) is Element of the carrier of the algebra of W
(n,RAS,W,p) is Element of the carrier of the algebra of W
Double (n,RAS,W,p) is Element of the carrier of the algebra of W
(n,RAS,W, the Element of the carrier of RAS,p) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m) is Element of the carrier of RAS
the Element of the carrier of RAS @ (n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m) is Element of the carrier of RAS
the MIDPOINT of RAS is V1() V4(K20( the carrier of RAS, the carrier of RAS)) V5( the carrier of RAS) Function-like V18(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) Element of K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS))
K20( the carrier of RAS, the carrier of RAS) is set
K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) is set
K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS)) is set
the MIDPOINT of RAS . ( the Element of the carrier of RAS,(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m)) is Element of the carrier of RAS
(n,RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m,( the Element of the carrier of RAS @ (n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
k is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),k) is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m,( the Element of the carrier of RAS @ (n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m))),k) is Element of the carrier of RAS
(n,RAS,W, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) is Element of the carrier of RAS
W . ( the Element of the carrier of RAS,(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m)) is Element of the carrier of the algebra of W
(n,RAS,W, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
W . ( the Element of the carrier of RAS,(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m)) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))),m) is Element of the carrier of the algebra of W
(n, the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m,( the Element of the carrier of RAS @ (n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),m))),m) is Element of the carrier of RAS
(n, the carrier of the algebra of W,p,k) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,p,k)) . W is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))),k) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))),k)) . W is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))),k) is Element of the carrier of RAS
(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS, the Element of the carrier of RAS) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,W, the Element of the carrier of RAS,p)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,W, the Element of the carrier of RAS,p)) is set
(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))))) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))))) is set
the Element of the carrier of RAS @ (n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m))))) is Element of the carrier of RAS
the MIDPOINT of RAS . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))))) is Element of the carrier of RAS
W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,(Double (n, the carrier of the algebra of W,p,m)))))) is Element of the carrier of the algebra of W
W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p))) is Element of the carrier of the algebra of W
Double (W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)))) is Element of the carrier of the algebra of W
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
a is Element of the carrier of RAS
p is Element of the carrier of RAS
a @ p is Element of the carrier of RAS
the MIDPOINT of RAS is V1() V4(K20( the carrier of RAS, the carrier of RAS)) V5( the carrier of RAS) Function-like V18(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) Element of K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS))
K20( the carrier of RAS, the carrier of RAS) is set
K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) is set
K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS)) is set
the MIDPOINT of RAS . (a,p) is Element of the carrier of RAS
pm is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
pm . m is set
(n,RAS,pm,m,(a @ p)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,pm,m,(a @ p))) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,pm,m,(a @ p))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,pm,m,(a @ p))) is set
(n,RAS,a,pm) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),pm) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),pm) is set
a @ (n,RAS,a,pm) is Element of the carrier of RAS
the MIDPOINT of RAS . (a,(n,RAS,a,pm)) is Element of the carrier of RAS
(n, the carrier of RAS,pm,m) is Element of the carrier of RAS
a @ (n, the carrier of RAS,pm,m) is Element of the carrier of RAS
the MIDPOINT of RAS . (a,(n, the carrier of RAS,pm,m)) is Element of the carrier of RAS
(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n, the carrier of the algebra of W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m) is Element of the carrier of the algebra of W
Double (n, the carrier of the algebra of W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m,(Double (n, the carrier of the algebra of W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,a,pm) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
pp is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m,(Double (n, the carrier of the algebra of W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m))),pp) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,(n,RAS,W,a,pm),pp) is Element of the carrier of the algebra of W
(n, the carrier of RAS,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m))),m) is Element of the carrier of RAS
W . (a,(n, the carrier of RAS,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m))),m)) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m,(Double (n, the carrier of the algebra of W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m))),m) is Element of the carrier of the algebra of W
W . (a,(n, the carrier of RAS,pm,m)) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,(n,RAS,W,a,pm),m) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),pp) is Element of the carrier of the algebra of W
(n, the carrier of RAS,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m))),pp) is Element of the carrier of RAS
W . (a,(n, the carrier of RAS,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m))),pp)) is Element of the carrier of the algebra of W
(n, the carrier of RAS,pm,pp) is Element of the carrier of RAS
W . (a,(n, the carrier of RAS,pm,pp)) is Element of the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m,(Double (n, the carrier of the algebra of W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))),m)))) is Element of the carrier of the algebra of W
W . (a,(n,RAS,a,pm)) is Element of the carrier of the algebra of W
(n,RAS,W,(n,RAS,W,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m))))) is Element of the carrier of the algebra of W
(n,RAS,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))) is set
W . (a,(n,RAS,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m))))) is Element of the carrier of the algebra of W
Double (W . (a,(n,RAS,a,(n,RAS,pm,m,(a @ (n, the carrier of RAS,pm,m)))))) is Element of the carrier of the algebra of W
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
the carrier of RAS is non empty set
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
W is Element of the carrier of RAS
a is Element of the carrier of RAS
W @ a is Element of the carrier of RAS
the MIDPOINT of RAS is V1() V4(K20( the carrier of RAS, the carrier of RAS)) V5( the carrier of RAS) Function-like V18(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) Element of K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS))
K20( the carrier of RAS, the carrier of RAS) is set
K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) is set
K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS)) is set
the MIDPOINT of RAS . (W,a) is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
p . m is set
(n,RAS,p,m,(W @ a)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,W,(n,RAS,p,m,(W @ a))) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS,W) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,W),(n,RAS,p,m,(W @ a))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,W),(n,RAS,p,m,(W @ a))) is set
(n,RAS,W,p) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,W),p) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,W),p) is set
W @ (n,RAS,W,p) is Element of the carrier of RAS
the MIDPOINT of RAS . (W,(n,RAS,W,p)) is Element of the carrier of RAS
(n, the carrier of RAS,p,m) is Element of the carrier of RAS
(n,RAS,p,m,W) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,W,(n,RAS,p,m,W)) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,W),(n,RAS,p,m,W)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,W),(n,RAS,p,m,W)) is set
(n,RAS,W,p) @ (n,RAS,W,(n,RAS,p,m,W)) is Element of the carrier of RAS
the MIDPOINT of RAS . ((n,RAS,W,p),(n,RAS,W,(n,RAS,p,m,W))) is Element of the carrier of RAS
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
a is Element of the carrier of RAS
p is Element of the carrier of RAS
pm is Element of the carrier of RAS
a @ pm is Element of the carrier of RAS
the MIDPOINT of RAS is V1() V4(K20( the carrier of RAS, the carrier of RAS)) V5( the carrier of RAS) Function-like V18(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) Element of K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS))
K20( the carrier of RAS, the carrier of RAS) is set
K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) is set
K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS)) is set
the MIDPOINT of RAS . (a,pm) is Element of the carrier of RAS
x is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n, the carrier of RAS,x,m) is Element of the carrier of RAS
(n, the carrier of RAS,x,m) @ p is Element of the carrier of RAS
the MIDPOINT of RAS . ((n, the carrier of RAS,x,m),p) is Element of the carrier of RAS
(n,RAS,x,m,((n, the carrier of RAS,x,m) @ p)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,x,m,((n, the carrier of RAS,x,m) @ p))) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,((n, the carrier of RAS,x,m) @ p))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,((n, the carrier of RAS,x,m) @ p))) is set
(n,RAS,a,x) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),x) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),x) is set
(n,RAS,x,m,p) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,x,m,p)) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,p)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,p)) is set
(n,RAS,a,x) @ (n,RAS,a,(n,RAS,x,m,p)) is Element of the carrier of RAS
the MIDPOINT of RAS . ((n,RAS,a,x),(n,RAS,a,(n,RAS,x,m,p))) is Element of the carrier of RAS
(n,RAS,x,m,pm) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,x,m,pm)) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,pm)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,pm)) is set
W . (a,(n,RAS,a,(n,RAS,x,m,pm))) is Element of the carrier of the algebra of W
the carrier of the algebra of W is non empty set
W . (a,(n,RAS,a,x)) is Element of the carrier of the algebra of W
W . (a,(n,RAS,a,(n,RAS,x,m,p))) is Element of the carrier of the algebra of W
(W . (a,(n,RAS,a,x))) + (W . (a,(n,RAS,a,(n,RAS,x,m,p)))) is Element of the carrier of the algebra of W
a @ (n,RAS,a,(n,RAS,x,m,pm)) is Element of the carrier of RAS
the MIDPOINT of RAS . (a,(n,RAS,a,(n,RAS,x,m,pm))) is Element of the carrier of RAS
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
(n + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
a is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n, the carrier of the algebra of W,a,m) is Element of the carrier of the algebra of W
Double (n, the carrier of the algebra of W,a,m) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),a,m,(Double (n, the carrier of the algebra of W,a,m))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),a,m,(Double (n, the carrier of the algebra of W,a,m)))) is Element of the carrier of the algebra of W
(n,RAS,W,a) is Element of the carrier of the algebra of W
Double (n,RAS,W,a) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),a,m,(n, the carrier of the algebra of W,a,m)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),a,m,(n, the carrier of the algebra of W,a,m)),x) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,a,x) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,a,m) + (n, the carrier of the algebra of W,a,m) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),a,m,((n, the carrier of the algebra of W,a,m) + (n, the carrier of the algebra of W,a,m))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),a,m,((n, the carrier of the algebra of W,a,m) + (n, the carrier of the algebra of W,a,m)))) is Element of the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),a,m,(n, the carrier of the algebra of W,a,m))) is Element of the carrier of the algebra of W
(n,RAS,W,a) + (n,RAS,W,( the carrier of the algebra of W,(n + 1),a,m,(n, the carrier of the algebra of W,a,m))) is Element of the carrier of the algebra of W
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
RAS is non empty MidSp-like (n)
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
(n + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
the carrier of RAS is non empty set
the Element of the carrier of RAS is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n, the carrier of the algebra of W,p,m) is Element of the carrier of the algebra of W
(n,RAS,W,p) is Element of the carrier of the algebra of W
pm is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,p,m) + pm is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm))) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),p,m,pm) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),p,m,pm)) is Element of the carrier of the algebra of W
(n,RAS,W,p) + (n,RAS,W,( the carrier of the algebra of W,(n + 1),p,m,pm)) is Element of the carrier of the algebra of W
(n,RAS,W, the Element of the carrier of RAS,p) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
( the Element of the carrier of RAS,pm) . W is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) @ (( the Element of the carrier of RAS,pm) . W) is Element of the carrier of RAS
the MIDPOINT of RAS is V1() V4(K20( the carrier of RAS, the carrier of RAS)) V5( the carrier of RAS) Function-like V18(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) Element of K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS))
K20( the carrier of RAS, the carrier of RAS) is set
K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) is set
K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS)) is set
the MIDPOINT of RAS . ((n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m),(( the Element of the carrier of RAS,pm) . W)) is Element of the carrier of RAS
x9 is Element of the carrier of RAS
x9 @ the Element of the carrier of RAS is Element of the carrier of RAS
the MIDPOINT of RAS . (x9, the Element of the carrier of RAS) is Element of the carrier of RAS
(n,RAS,W, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
W . ( the Element of the carrier of RAS,(( the Element of the carrier of RAS,pm) . W)) is Element of the carrier of the algebra of W
W . ( the Element of the carrier of RAS,x9) is Element of the carrier of the algebra of W
W . ( the Element of the carrier of RAS,(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m)) is Element of the carrier of the algebra of W
(W . ( the Element of the carrier of RAS,(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m))) + (W . ( the Element of the carrier of RAS,(( the Element of the carrier of RAS,pm) . W))) is Element of the carrier of the algebra of W
(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,x9) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
i is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,x9),i) is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm))),i) is Element of the carrier of RAS
( the Element of the carrier of RAS,((n, the carrier of the algebra of W,p,m) + pm)) . W is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm)),m) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm)),m)) . W is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),i) is Element of the carrier of RAS
(n, the carrier of the algebra of W,p,i) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,p,i)) . W is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm)),i) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,((n, the carrier of the algebra of W,p,m) + pm)),i)) . W is Element of the carrier of RAS
(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,x9)) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS, the Element of the carrier of RAS) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,x9)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,x9)) is set
W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,x9))) is Element of the carrier of the algebra of W
(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,pm)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
qq is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W)),qq) is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,m,pm)),qq) is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,pm),m) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,pm),m)) . W is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),qq) is Element of the carrier of RAS
(n, the carrier of the algebra of W,p,qq) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,p,qq)) . W is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,pm),qq) is Element of the carrier of the algebra of W
( the Element of the carrier of RAS,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),p,m,pm),qq)) . W is Element of the carrier of RAS
(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,((n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) @ (( the Element of the carrier of RAS,pm) . W))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,((n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) @ (( the Element of the carrier of RAS,pm) . W)))) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,((n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) @ (( the Element of the carrier of RAS,pm) . W)))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,((n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) @ (( the Element of the carrier of RAS,pm) . W)))) is set
(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,W, the Element of the carrier of RAS,p)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,W, the Element of the carrier of RAS,p)) is set
(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W))) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W))) is set
(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)) @ (n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W))) is Element of the carrier of RAS
the MIDPOINT of RAS . ((n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)),(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W)))) is Element of the carrier of RAS
W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p))) is Element of the carrier of the algebra of W
W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W)))) is Element of the carrier of the algebra of W
(W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p)))) + (W . ( the Element of the carrier of RAS,(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),m,(( the Element of the carrier of RAS,pm) . W))))) is Element of the carrier of the algebra of W
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
a is Element of the carrier of RAS
p is Element of the carrier of RAS
pm is Element of the carrier of RAS
p @ pm is Element of the carrier of RAS
the MIDPOINT of RAS is V1() V4(K20( the carrier of RAS, the carrier of RAS)) V5( the carrier of RAS) Function-like V18(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) Element of K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS))
K20( the carrier of RAS, the carrier of RAS) is set
K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS) is set
K19(K20(K20( the carrier of RAS, the carrier of RAS), the carrier of RAS)) is set
the MIDPOINT of RAS . (p,pm) is Element of the carrier of RAS
x is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n, the carrier of RAS,x,m) is Element of the carrier of RAS
(n,RAS,x,m,(p @ pm)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,x,m,(p @ pm))) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,(p @ pm))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,(p @ pm))) is set
(n,RAS,a,x) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),x) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),x) is set
(n,RAS,x,m,pm) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,x,m,pm)) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,pm)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,pm)) is set
(n,RAS,a,x) @ (n,RAS,a,(n,RAS,x,m,pm)) is Element of the carrier of RAS
the MIDPOINT of RAS . ((n,RAS,a,x),(n,RAS,a,(n,RAS,x,m,pm))) is Element of the carrier of RAS
(n,RAS,W,a,x) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
W . (a,pm) is Element of the carrier of the algebra of W
(n, the carrier of RAS,x,m) @ pm is Element of the carrier of RAS
the MIDPOINT of RAS . ((n, the carrier of RAS,x,m),pm) is Element of the carrier of RAS
k is Element of the carrier of RAS
k @ a is Element of the carrier of RAS
the MIDPOINT of RAS . (k,a) is Element of the carrier of RAS
(n,RAS,W,a,(n,RAS,W,a,x)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
W . (a,k) is Element of the carrier of the algebra of W
W . (a,(n, the carrier of RAS,x,m)) is Element of the carrier of the algebra of W
(W . (a,(n, the carrier of RAS,x,m))) + (W . (a,pm)) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,(n,RAS,W,a,x),m) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm)) is Element of the carrier of the algebra of W
(n,RAS,x,m,k) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm)))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,a,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm))))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
i is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of RAS,(n,RAS,x,m,k),i) is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W,a,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm))))),i) is Element of the carrier of RAS
(a,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm)))) . W is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm)))),m) is Element of the carrier of the algebra of W
(a,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm)))),m)) . W is Element of the carrier of RAS
(n, the carrier of RAS,x,i) is Element of the carrier of RAS
(n, the carrier of the algebra of W,(n,RAS,W,a,x),i) is Element of the carrier of the algebra of W
(a,(n, the carrier of the algebra of W,(n,RAS,W,a,x),i)) . W is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm)))),i) is Element of the carrier of the algebra of W
(a,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm)))),i)) . W is Element of the carrier of RAS
(n,RAS,W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,((n, the carrier of the algebra of W,(n,RAS,W,a,x),m) + (W . (a,pm))))) is Element of the carrier of the algebra of W
(n,RAS,a,(n,RAS,x,m,k)) is Element of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,k)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,x,m,k)) is set
W . (a,(n,RAS,a,(n,RAS,x,m,k))) is Element of the carrier of the algebra of W
(a,(W . (a,pm))) . W is Element of the carrier of RAS
( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,a,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm)))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
i is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of RAS,(n,RAS,x,m,pm),i) is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W,a,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm)))),i) is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm))),m) is Element of the carrier of the algebra of W
(a,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm))),m)) . W is Element of the carrier of RAS
(n, the carrier of RAS,x,i) is Element of the carrier of RAS
(n, the carrier of the algebra of W,(n,RAS,W,a,x),i) is Element of the carrier of the algebra of W
(a,(n, the carrier of the algebra of W,(n,RAS,W,a,x),i)) . W is Element of the carrier of RAS
(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm))),i) is Element of the carrier of the algebra of W
(a,(n, the carrier of the algebra of W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm))),i)) . W is Element of the carrier of RAS
(n,RAS,W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,x),m,(W . (a,pm)))) is Element of the carrier of the algebra of W
W . (a,(n,RAS,a,(n,RAS,x,m,pm))) is Element of the carrier of the algebra of W
(n,RAS,W,(n,RAS,W,a,x)) is Element of the carrier of the algebra of W
W . (a,(n,RAS,a,x)) is Element of the carrier of the algebra of W
(W . (a,(n,RAS,a,x))) + (W . (a,(n,RAS,a,(n,RAS,x,m,pm)))) is Element of the carrier of the algebra of W
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty MidSp-like (n)
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
W is Element of the carrier of RAS
a is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n, the carrier of RAS,a,m) is Element of the carrier of RAS
(n,RAS,a,(m + 1),(n, the carrier of RAS,a,m)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
p is ATLAS-like AtlasStr over RAS
the algebra of p is non empty L7()
the carrier of the algebra of p is non empty set
(n + 1) -tuples_on the carrier of the algebra of p is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of p
(n,RAS,p,W,a) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n,RAS,p,W,(n,RAS,a,(m + 1),(n, the carrier of RAS,a,m))) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
pm is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n, the carrier of the algebra of p,pm,m) is Element of the carrier of the algebra of p
( the carrier of the algebra of p,(n + 1),pm,(m + 1),(n, the carrier of the algebra of p,pm,m)) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
x is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n,RAS,a,x,(n, the carrier of RAS,a,m)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,p,W,(n,RAS,a,x,(n, the carrier of RAS,a,m))) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
( the carrier of the algebra of p,(n + 1),pm,x,(n, the carrier of the algebra of p,pm,m)) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
k is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
(n, the carrier of the algebra of p,(n,RAS,p,W,(n,RAS,a,x,(n, the carrier of RAS,a,m))),k) is Element of the carrier of the algebra of p
(n, the carrier of the algebra of p,( the carrier of the algebra of p,(n + 1),pm,x,(n, the carrier of the algebra of p,pm,m)),k) is Element of the carrier of the algebra of p
(n, the carrier of RAS,(n,RAS,a,x,(n, the carrier of RAS,a,m)),k) is Element of the carrier of RAS
p . (W,(n, the carrier of RAS,(n,RAS,a,x,(n, the carrier of RAS,a,m)),k)) is Element of the carrier of the algebra of p
p . (W,(n, the carrier of RAS,a,m)) is Element of the carrier of the algebra of p
(n, the carrier of RAS,(n,RAS,a,x,(n, the carrier of RAS,a,m)),k) is Element of the carrier of RAS
p . (W,(n, the carrier of RAS,(n,RAS,a,x,(n, the carrier of RAS,a,m)),k)) is Element of the carrier of the algebra of p
(n, the carrier of RAS,a,k) is Element of the carrier of RAS
p . (W,(n, the carrier of RAS,a,k)) is Element of the carrier of the algebra of p
(n, the carrier of the algebra of p,pm,k) is Element of the carrier of the algebra of p
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty MidSp-like (n)
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
W is Element of the carrier of RAS
a is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n, the carrier of RAS,a,m) is Element of the carrier of RAS
(n,RAS,a,(m + 1),(n, the carrier of RAS,a,m)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
p is ATLAS-like AtlasStr over RAS
the algebra of p is non empty L7()
the carrier of the algebra of p is non empty set
(n + 1) -tuples_on the carrier of the algebra of p is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of p
pm is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n,RAS,p,W,pm) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n, the carrier of the algebra of p,pm,m) is Element of the carrier of the algebra of p
( the carrier of the algebra of p,(n + 1),pm,(m + 1),(n, the carrier of the algebra of p,pm,m)) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n,RAS,p,W,( the carrier of the algebra of p,(n + 1),pm,(m + 1),(n, the carrier of the algebra of p,pm,m))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,p,W,a) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
(n,RAS,p,W,(n,RAS,a,(m + 1),(n, the carrier of RAS,a,m))) is V1() V4( NAT ) V5( the carrier of the algebra of p) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of p
n is V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
m is V24() V25() V26() V30() V31() ext-real non negative V49() (n)
m + 1 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
RAS is non empty MidSp-like (n)
W is ATLAS-like AtlasStr over RAS
the algebra of W is non empty L7()
the carrier of the algebra of W is non empty set
(n + 1) -tuples_on the carrier of the algebra of W is functional non empty FinSequence-membered FinSequenceSet of the carrier of the algebra of W
0. W is Element of the carrier of the algebra of W
the carrier of RAS is non empty set
the Element of the carrier of RAS is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n, the carrier of the algebra of W,p,m) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),p,(m + 1),(n, the carrier of the algebra of W,p,m)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),p,(m + 1),(n, the carrier of the algebra of W,p,m))) is Element of the carrier of the algebra of W
(n,RAS,W, the Element of the carrier of RAS,p) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
( the Element of the carrier of RAS,(0. W)) . W is Element of the carrier of RAS
(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m) is Element of the carrier of RAS
(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),(m + 1),(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS, the Element of the carrier of RAS,(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),(m + 1),(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m))) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS, the Element of the carrier of RAS) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),(m + 1),(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS, the Element of the carrier of RAS),(n,RAS,(n,RAS,W, the Element of the carrier of RAS,p),(m + 1),(n, the carrier of RAS,(n,RAS,W, the Element of the carrier of RAS,p),m))) is set
(n,RAS,W, the Element of the carrier of RAS,( the carrier of the algebra of W,(n + 1),p,(m + 1),(n, the carrier of the algebra of W,p,m))) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
the carrier of RAS is non empty set
(n + 1) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
a is Element of the carrier of RAS
p is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n, the carrier of RAS,p,m) is Element of the carrier of RAS
pm is Element of the carrier of RAS
(n,RAS,p,(m + 1),pm) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,a,(n,RAS,p,(m + 1),pm)) is Element of the carrier of RAS
n + 2 is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
the of RAS is V1() V4((n + 2) -tuples_on the carrier of RAS) V5( the carrier of RAS) Function-like V18((n + 2) -tuples_on the carrier of RAS, the carrier of RAS) Element of K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS))
(n + 2) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS) is set
K19(K20(((n + 2) -tuples_on the carrier of RAS), the carrier of RAS)) is set
(n,RAS,a) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1) FinSequence-like Element of 1 -tuples_on the carrier of RAS
1 -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
(n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,p,(m + 1),pm)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(1 + (n + 1)) FinSequence-like Element of (1 + (n + 1)) -tuples_on the carrier of RAS
1 + (n + 1) is non empty V24() V25() V26() V30() V31() ext-real non negative V49() Element of NAT
(1 + (n + 1)) -tuples_on the carrier of RAS is functional non empty FinSequence-membered FinSequenceSet of the carrier of RAS
the of RAS . (n,RAS,1,(n + 1),(n,RAS,a),(n,RAS,p,(m + 1),pm)) is set
(n,RAS,W,a,p) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
W . (a,a) is Element of the carrier of the algebra of W
(n, the carrier of the algebra of W,(n,RAS,W,a,p),m) is Element of the carrier of the algebra of W
( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,p),(m + 1),(n, the carrier of the algebra of W,(n,RAS,W,a,p),m)) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W
(n,RAS,W,( the carrier of the algebra of W,(n + 1),(n,RAS,W,a,p),(m + 1),(n, the carrier of the algebra of W,(n,RAS,W,a,p),m))) is Element of the carrier of the algebra of W
(n,RAS,p,(m + 1),(n, the carrier of RAS,p,m)) is V1() V4( NAT ) V5( the carrier of RAS) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of RAS
(n,RAS,W,a,(n,RAS,p,(m + 1),(n, the carrier of RAS,p,m))) is V1() V4( NAT ) V5( the carrier of the algebra of W) Function-like V42(n + 1) FinSequence-like Element of (n + 1) -tuples_on the carrier of the algebra of W