:: BINOM semantic presentation

REAL is set
NAT is non empty V24() V25() V26() V35() V40() V41() Element of bool REAL
bool REAL is set
COMPLEX is set
NAT is non empty V24() V25() V26() V35() V40() V41() set
bool NAT is V35() set
bool NAT is V35() set
RAT is set
INT is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
K334() is non empty strict multMagma
the carrier of K334() is non empty set
K339() is non empty strict unital Group-like associative commutative V159() V160() V161() V162() V163() V164() multMagma
K340() is non empty strict associative commutative V162() V163() V164() M13(K339())
K341() is non empty strict unital associative commutative V162() V163() V164() V165() M16(K339(),K340())
K343() is non empty strict unital associative commutative multMagma
K344() is non empty strict unital associative commutative V165() M13(K343())
{} is functional empty V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() V40() V42( {} ) FinSequence-membered ext-real non positive non negative set
2 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
0 is functional empty V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() V40() V42( {} ) FinSequence-membered ext-real non positive non negative Element of NAT
3 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
Seg 1 is non empty trivial V35() V42(1) Element of bool NAT
{1} is non empty trivial V42(1) set
Seg 2 is non empty V35() V42(2) Element of bool NAT
{1,2} is non empty set
R is non empty addLoopStr
a is non empty right_add-cancelable Abelian addLoopStr
the carrier of a is non empty set
b is right_add-cancelable Element of the carrier of a
n is right_add-cancelable Element of the carrier of a
b + n is right_add-cancelable Element of the carrier of a
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (b,n) is right_add-cancelable Element of the carrier of a
[b,n] is V15() set
the addF of a . [b,n] is set
n is right_add-cancelable Element of the carrier of a
b + n is right_add-cancelable Element of the carrier of a
the addF of a . (b,n) is right_add-cancelable Element of the carrier of a
[b,n] is V15() set
the addF of a . [b,n] is set
b + n is right_add-cancelable Element of the carrier of a
b + n is right_add-cancelable Element of the carrier of a
R is non empty addLoopStr
a is non empty left_add-cancelable Abelian addLoopStr
the carrier of a is non empty set
n is left_add-cancelable Element of the carrier of a
b is left_add-cancelable Element of the carrier of a
n + b is left_add-cancelable Element of the carrier of a
the addF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the addF of a . (n,b) is left_add-cancelable Element of the carrier of a
[n,b] is V15() set
the addF of a . [n,b] is set
n is left_add-cancelable Element of the carrier of a
n + b is left_add-cancelable Element of the carrier of a
the addF of a . (n,b) is left_add-cancelable Element of the carrier of a
[n,b] is V15() set
the addF of a . [n,b] is set
n + b is left_add-cancelable Element of the carrier of a
n + b is left_add-cancelable Element of the carrier of a
R is non empty addLoopStr
the non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable left_zeroed add-left-invertible add-right-invertible Loop-like unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
R is non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
the carrier of R is non empty set
0. R is V54(R) left_add-cancelable Element of the carrier of R
a is left_add-cancelable Element of the carrier of R
(0. R) * a is left_add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((0. R),a) is left_add-cancelable Element of the carrier of R
[(0. R),a] is V15() set
the multF of R . [(0. R),a] is set
(0. R) + (0. R) is left_add-cancelable Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the addF of R . ((0. R),(0. R)) is left_add-cancelable Element of the carrier of R
[(0. R),(0. R)] is V15() set
the addF of R . [(0. R),(0. R)] is set
((0. R) + (0. R)) * a is left_add-cancelable Element of the carrier of R
the multF of R . (((0. R) + (0. R)),a) is left_add-cancelable Element of the carrier of R
[((0. R) + (0. R)),a] is V15() set
the multF of R . [((0. R) + (0. R)),a] is set
((0. R) * a) + ((0. R) * a) is left_add-cancelable Element of the carrier of R
the addF of R . (((0. R) * a),((0. R) * a)) is left_add-cancelable Element of the carrier of R
[((0. R) * a),((0. R) * a)] is V15() set
the addF of R . [((0. R) * a),((0. R) * a)] is set
((0. R) * a) + (0. R) is left_add-cancelable Element of the carrier of R
the addF of R . (((0. R) * a),(0. R)) is left_add-cancelable Element of the carrier of R
[((0. R) * a),(0. R)] is V15() set
the addF of R . [((0. R) * a),(0. R)] is set
R is non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr
the carrier of R is non empty set
0. R is V54(R) right_add-cancelable Element of the carrier of R
a is right_add-cancelable Element of the carrier of R
a * (0. R) is right_add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . (a,(0. R)) is right_add-cancelable Element of the carrier of R
[a,(0. R)] is V15() set
the multF of R . [a,(0. R)] is set
(0. R) + (0. R) is right_add-cancelable Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the addF of R . ((0. R),(0. R)) is right_add-cancelable Element of the carrier of R
[(0. R),(0. R)] is V15() set
the addF of R . [(0. R),(0. R)] is set
a * ((0. R) + (0. R)) is right_add-cancelable Element of the carrier of R
the multF of R . (a,((0. R) + (0. R))) is right_add-cancelable Element of the carrier of R
[a,((0. R) + (0. R))] is V15() set
the multF of R . [a,((0. R) + (0. R))] is set
(a * (0. R)) + (a * (0. R)) is right_add-cancelable Element of the carrier of R
the addF of R . ((a * (0. R)),(a * (0. R))) is right_add-cancelable Element of the carrier of R
[(a * (0. R)),(a * (0. R))] is V15() set
the addF of R . [(a * (0. R)),(a * (0. R))] is set
(0. R) + (a * (0. R)) is right_add-cancelable Element of the carrier of R
the addF of R . ((0. R),(a * (0. R))) is right_add-cancelable Element of the carrier of R
[(0. R),(a * (0. R))] is V15() set
the addF of R . [(0. R),(a * (0. R))] is set
a is non empty set
R is non empty set
[:R,a:] is set
[:[:R,a:],a:] is set
bool [:[:R,a:],a:] is set
[:NAT,R:] is V35() set
[:[:NAT,R:],a:] is V35() set
bool [:[:NAT,R:],a:] is V35() set
b is Element of a
n is V1() V4([:R,a:]) V5(a) Function-like quasi_total Element of bool [:[:R,a:],a:]
[:NAT,a:] is V35() set
bool [:NAT,a:] is V35() set
n is Element of R
G2 is Element of a
n . (n,G2) is Element of a
[n,G2] is V15() set
n . [n,G2] is set
G1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
G1 . 0 is Element of a
Funcs (NAT,a) is non empty FUNCTION_DOMAIN of NAT ,a
[:R,(Funcs (NAT,a)):] is set
bool [:R,(Funcs (NAT,a)):] is set
{ [b₁,b₂] where b₁ is Element of R, b₂ is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a) : ex b₃ being V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:] st
( b₃ = b₂ & b₃ . 0 = b & ( for b₄ being V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT holds b₃ . (b₄ + 1) = n . (b₁,(b₃ . b₄)) ) ) } is set
G1 is set
G2 is set
[G1,G2] is V15() set
F1 is set
[G1,F1] is V15() set
F2 is Element of R
F is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[F2,F] is V15() set
i is Element of R
j is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[i,j] is V15() set
x is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
x . 0 is Element of a
x is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
x . 0 is Element of a
r1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r1 . 0 is Element of a
r1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r1 . 0 is Element of a
[F2,F] `1 is set
[G1,G2] `1 is set
[G1,F1] `1 is set
[i,j] `1 is set
r2 is set
m1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
x . m1 is Element of a
r1 . m1 is Element of a
m1 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
x . (m1 + 1) is Element of a
n . (i,(x . m1)) is Element of a
[i,(x . m1)] is V15() set
n . [i,(x . m1)] is set
r1 . (m1 + 1) is Element of a
x . r2 is set
r is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
r1 . r is Element of a
r1 . r2 is set
dom x is Element of bool NAT
dom r1 is Element of bool NAT
[G1,G2] `2 is set
[F2,F] `2 is set
[i,j] `2 is set
[G1,F1] `2 is set
G1 is set
G2 is Element of R
F1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[G2,F1] is V15() set
F2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
F2 . 0 is Element of a
G1 is V1() V4(R) V5( Funcs (NAT,a)) Element of bool [:R,(Funcs (NAT,a)):]
dom G1 is Element of bool R
bool R is set
G2 is set
F1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
F1 . 0 is Element of a
F2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[G2,F2] is V15() set
G2 is set
G2 is V1() V4(R) V5( Funcs (NAT,a)) Function-like quasi_total Element of bool [:R,(Funcs (NAT,a)):]
F1 is Element of R
G2 . F1 is Element of Funcs (NAT,a)
dom G2 is Element of bool R
[F1,(G2 . F1)] is V15() set
F2 is Element of R
F is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[F2,F] is V15() set
[F1,(G2 . F1)] `2 is set
[F2,F] `2 is set
[F1,(G2 . F1)] `1 is set
[F2,F] `1 is set
i is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
i . 0 is Element of a
F1 is Element of R
G2 . F1 is Element of Funcs (NAT,a)
n is V1() V4(R) V5( Funcs (NAT,a)) Function-like quasi_total Element of bool [:R,(Funcs (NAT,a)):]
n is V1() V4(R) V5( Funcs (NAT,a)) Function-like quasi_total Element of bool [:R,(Funcs (NAT,a)):]
{ [[b₁,b₂],b₃] where b₁ is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT , b₂ is Element of R, b₃ is Element of a : ex b₄ being V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:] st
( b₄ = n . b₂ & b₃ = b₄ . b₁ ) } is set
G2 is set
F1 is set
[G2,F1] is V15() set
F2 is set
[G2,F2] is V15() set
F is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
i is Element of R
[F,i] is V15() set
j is Element of a
[[F,i],j] is V15() set
n . i is Element of Funcs (NAT,a)
x is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
r1 is Element of R
[x,r1] is V15() set
r2 is Element of a
[[x,r1],r2] is V15() set
n . r1 is Element of Funcs (NAT,a)
[[F,i],j] `1 is set
[G2,F1] `1 is set
[G2,F2] `1 is set
[[x,r1],r2] `1 is set
[F,i] `2 is set
[x,r1] `2 is set
[F,i] `1 is set
[x,r1] `1 is set
[G2,F1] `2 is set
[G2,F2] `2 is set
r is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r . F is Element of a
m1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
m1 . x is Element of a
G2 is set
F1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
F2 is Element of R
[F1,F2] is V15() set
F is Element of a
[[F1,F2],F] is V15() set
n . F2 is Element of Funcs (NAT,a)
G2 is V1() V4([:NAT,R:]) V5(a) Element of bool [:[:NAT,R:],a:]
dom G2 is V1() V4( NAT ) V5(R) Element of bool [:NAT,R:]
bool [:NAT,R:] is V35() set
F1 is set
F2 is set
F is set
[F2,F] is V15() set
i is Element of R
n . i is Element of Funcs (NAT,a)
x is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
x . 0 is Element of a
j is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
x . j is Element of a
r2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r1 is Element of a
r2 . j is Element of a
r1 is Element of a
[F1,r1] is V15() set
r2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r2 . j is Element of a
F1 is set
F1 is V1() V4([:NAT,R:]) V5(a) Function-like quasi_total Element of bool [:[:NAT,R:],a:]
F2 is Element of R
F1 . (0,F2) is Element of a
[0,F2] is V15() set
F1 . [0,F2] is set
n . F2 is Element of Funcs (NAT,a)
F is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
F . 0 is Element of a
i is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
i + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
[(i + 1),F2] is V15() set
dom F1 is V1() V4( NAT ) V5(R) Element of bool [:NAT,R:]
j is set
[[(i + 1),F2],j] is V15() set
[i,F2] is V15() set
x is set
[[i,F2],x] is V15() set
r1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
r2 is Element of R
[r1,r2] is V15() set
r is Element of a
[[r1,r2],r] is V15() set
n . r2 is Element of Funcs (NAT,a)
[[(i + 1),F2],j] `2 is set
[[r1,r2],r] `2 is set
m1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
m2 is Element of R
[m1,m2] is V15() set
l2 is Element of a
[[m1,m2],l2] is V15() set
n . m2 is Element of Funcs (NAT,a)
[[i,F2],x] `2 is set
[[m1,m2],l2] `2 is set
[[(i + 1),F2],j] `1 is set
[[r1,r2],r] `1 is set
[r1,r2] `2 is set
[(i + 1),F2] `2 is set
[[i,F2],x] `1 is set
[[m1,m2],l2] `1 is set
[m1,m2] `1 is set
[i,F2] `1 is set
[m1,m2] `2 is set
[i,F2] `2 is set
[r1,r2] `1 is set
[(i + 1),F2] `1 is set
F1 . ((i + 1),F2) is Element of a
F1 . [(i + 1),F2] is set
F . (i + 1) is Element of a
n . (F2,l2) is Element of a
[F2,l2] is V15() set
n . [F2,l2] is set
F1 . (i,F2) is Element of a
F1 . [i,F2] is set
n . (F2,(F1 . (i,F2))) is Element of a
[F2,(F1 . (i,F2))] is V15() set
n . [F2,(F1 . (i,F2))] is set
l1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
l1 . r1 is Element of a
l1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
l1 . m1 is Element of a
i is set
[[0,F2],i] is V15() set
j is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
x is Element of R
[j,x] is V15() set
r1 is Element of a
[[j,x],r1] is V15() set
n . x is Element of Funcs (NAT,a)
[[0,F2],i] `2 is set
[[j,x],r1] `2 is set
[[0,F2],i] `1 is set
[[j,x],r1] `1 is set
[j,x] `2 is set
[0,F2] `2 is set
[j,x] `1 is set
[0,F2] `1 is set
r2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
r2 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
F1 . ((r2 + 1),F2) is Element of a
[(r2 + 1),F2] is V15() set
F1 . [(r2 + 1),F2] is set
F1 . (r2,F2) is Element of a
[r2,F2] is V15() set
F1 . [r2,F2] is set
n . (F2,(F1 . (r2,F2))) is Element of a
[F2,(F1 . (r2,F2))] is V15() set
n . [F2,(F1 . (r2,F2))] is set
r is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r . j is Element of a
F2 is Element of R
F1 . (0,F2) is Element of a
[0,F2] is V15() set
F1 . [0,F2] is set
i is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
i + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
F is Element of R
F1 . ((i + 1),F) is Element of a
[(i + 1),F] is V15() set
F1 . [(i + 1),F] is set
F1 . (i,F) is Element of a
[i,F] is V15() set
F1 . [i,F] is set
n . (F,(F1 . (i,F))) is Element of a
[F,(F1 . (i,F))] is V15() set
n . [F,(F1 . (i,F))] is set
a is non empty set
R is non empty set
[:a,R:] is set
[:[:a,R:],a:] is set
bool [:[:a,R:],a:] is set
[:R,NAT:] is V35() set
[:[:R,NAT:],a:] is V35() set
bool [:[:R,NAT:],a:] is V35() set
b is Element of a
n is V1() V4([:a,R:]) V5(a) Function-like quasi_total Element of bool [:[:a,R:],a:]
[:NAT,a:] is V35() set
bool [:NAT,a:] is V35() set
n is Element of R
G2 is Element of a
n . (G2,n) is Element of a
[G2,n] is V15() set
n . [G2,n] is set
G1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
G1 . 0 is Element of a
Funcs (NAT,a) is non empty FUNCTION_DOMAIN of NAT ,a
[:R,(Funcs (NAT,a)):] is set
bool [:R,(Funcs (NAT,a)):] is set
{ [b₁,b₂] where b₁ is Element of R, b₂ is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a) : ex b₃ being V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:] st
( b₃ = b₂ & b₃ . 0 = b & ( for b₄ being V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT holds b₃ . (b₄ + 1) = n . ((b₃ . b₄),b₁) ) ) } is set
G1 is set
G2 is set
[G1,G2] is V15() set
F1 is set
[G1,F1] is V15() set
F2 is Element of R
F is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[F2,F] is V15() set
i is Element of R
j is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[i,j] is V15() set
x is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
x . 0 is Element of a
x is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
x . 0 is Element of a
r1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r1 . 0 is Element of a
r1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r1 . 0 is Element of a
[F2,F] `1 is set
[G1,G2] `1 is set
[G1,F1] `1 is set
[i,j] `1 is set
r2 is set
m1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
x . m1 is Element of a
r1 . m1 is Element of a
m1 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
x . (m1 + 1) is Element of a
n . ((x . m1),i) is Element of a
[(x . m1),i] is V15() set
n . [(x . m1),i] is set
r1 . (m1 + 1) is Element of a
x . r2 is set
r is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
r1 . r is Element of a
r1 . r2 is set
dom x is Element of bool NAT
dom r1 is Element of bool NAT
[G1,G2] `2 is set
[F2,F] `2 is set
[i,j] `2 is set
[G1,F1] `2 is set
G1 is set
G2 is Element of R
F1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[G2,F1] is V15() set
F2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
F2 . 0 is Element of a
G1 is V1() V4(R) V5( Funcs (NAT,a)) Element of bool [:R,(Funcs (NAT,a)):]
dom G1 is Element of bool R
bool R is set
G2 is set
F1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
F1 . 0 is Element of a
F2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[G2,F2] is V15() set
G2 is set
G2 is V1() V4(R) V5( Funcs (NAT,a)) Function-like quasi_total Element of bool [:R,(Funcs (NAT,a)):]
F1 is Element of R
G2 . F1 is Element of Funcs (NAT,a)
dom G2 is Element of bool R
[F1,(G2 . F1)] is V15() set
F2 is Element of R
F is V1() V4( NAT ) V5(a) Function-like quasi_total Element of Funcs (NAT,a)
[F2,F] is V15() set
[F1,(G2 . F1)] `2 is set
[F2,F] `2 is set
[F1,(G2 . F1)] `1 is set
[F2,F] `1 is set
i is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
i . 0 is Element of a
F1 is Element of R
G2 . F1 is Element of Funcs (NAT,a)
n is V1() V4(R) V5( Funcs (NAT,a)) Function-like quasi_total Element of bool [:R,(Funcs (NAT,a)):]
n is V1() V4(R) V5( Funcs (NAT,a)) Function-like quasi_total Element of bool [:R,(Funcs (NAT,a)):]
{ [[b₂,b₁],b₃] where b₁ is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT , b₂ is Element of R, b₃ is Element of a : ex b₄ being V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:] st
( b₄ = n . b₂ & b₃ = b₄ . b₁ ) } is set
G2 is set
F1 is set
[G2,F1] is V15() set
F2 is set
[G2,F2] is V15() set
i is Element of R
F is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
[i,F] is V15() set
j is Element of a
[[i,F],j] is V15() set
n . i is Element of Funcs (NAT,a)
r1 is Element of R
x is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
[r1,x] is V15() set
r2 is Element of a
[[r1,x],r2] is V15() set
n . r1 is Element of Funcs (NAT,a)
[[i,F],j] `1 is set
[G2,F1] `1 is set
[G2,F2] `1 is set
[[r1,x],r2] `1 is set
[i,F] `2 is set
[r1,x] `2 is set
[i,F] `1 is set
[r1,x] `1 is set
[G2,F1] `2 is set
[G2,F2] `2 is set
r is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r . F is Element of a
m1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
m1 . x is Element of a
G2 is set
F2 is Element of R
F1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
[F2,F1] is V15() set
F is Element of a
[[F2,F1],F] is V15() set
n . F2 is Element of Funcs (NAT,a)
G2 is V1() V4([:R,NAT:]) V5(a) Element of bool [:[:R,NAT:],a:]
dom G2 is V1() V4(R) V5( NAT ) Element of bool [:R,NAT:]
bool [:R,NAT:] is V35() set
F1 is set
F2 is set
F is set
[F2,F] is V15() set
i is Element of R
n . i is Element of Funcs (NAT,a)
x is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
x . 0 is Element of a
j is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
x . j is Element of a
r2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r1 is Element of a
r2 . j is Element of a
r1 is Element of a
[F1,r1] is V15() set
r2 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r2 . j is Element of a
F1 is set
F1 is V1() V4([:R,NAT:]) V5(a) Function-like quasi_total Element of bool [:[:R,NAT:],a:]
F2 is Element of R
F1 . (F2,0) is Element of a
[F2,0] is V15() set
F1 . [F2,0] is set
n . F2 is Element of Funcs (NAT,a)
F is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
F . 0 is Element of a
i is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
i + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
[F2,(i + 1)] is V15() set
dom F1 is V1() V4(R) V5( NAT ) Element of bool [:R,NAT:]
j is set
[[F2,(i + 1)],j] is V15() set
[F2,i] is V15() set
x is set
[[F2,i],x] is V15() set
r2 is Element of R
r1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
[r2,r1] is V15() set
r is Element of a
[[r2,r1],r] is V15() set
n . r2 is Element of Funcs (NAT,a)
[[F2,i],x] `2 is set
[[r2,r1],r] `2 is set
[[F2,i],x] `1 is set
[[r2,r1],r] `1 is set
[r2,r1] `2 is set
[F2,i] `2 is set
m1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
m1 . r1 is Element of a
m1 is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
m1 . r1 is Element of a
l2 is Element of R
m2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
[l2,m2] is V15() set
l1 is Element of a
[[l2,m2],l1] is V15() set
n . l2 is Element of Funcs (NAT,a)
[[F2,(i + 1)],j] `1 is set
[[l2,m2],l1] `1 is set
[l2,m2] `2 is set
[F2,(i + 1)] `2 is set
[r2,r1] `1 is set
[F2,i] `1 is set
[l2,m2] `1 is set
[F2,(i + 1)] `1 is set
[[F2,(i + 1)],j] `2 is set
[[l2,m2],l1] `2 is set
F1 . (F2,(i + 1)) is Element of a
F1 . [F2,(i + 1)] is set
F . m2 is Element of a
n . ((m1 . r1),F2) is Element of a
[(m1 . r1),F2] is V15() set
n . [(m1 . r1),F2] is set
F1 . (F2,i) is Element of a
F1 . [F2,i] is set
n . ((F1 . (F2,i)),F2) is Element of a
[(F1 . (F2,i)),F2] is V15() set
n . [(F1 . (F2,i)),F2] is set
c₂₁ is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
c₂₁ . m2 is Element of a
i is set
[[F2,0],i] is V15() set
x is Element of R
j is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
[x,j] is V15() set
r1 is Element of a
[[x,j],r1] is V15() set
n . x is Element of Funcs (NAT,a)
[[F2,0],i] `2 is set
[[x,j],r1] `2 is set
[[F2,0],i] `1 is set
[[x,j],r1] `1 is set
[x,j] `1 is set
[F2,0] `1 is set
[x,j] `2 is set
[F2,0] `2 is set
r2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
r2 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
F1 . (F2,(r2 + 1)) is Element of a
[F2,(r2 + 1)] is V15() set
F1 . [F2,(r2 + 1)] is set
F1 . (F2,r2) is Element of a
[F2,r2] is V15() set
F1 . [F2,r2] is set
n . ((F1 . (F2,r2)),F2) is Element of a
[(F1 . (F2,r2)),F2] is V15() set
n . [(F1 . (F2,r2)),F2] is set
r is V1() V4( NAT ) V5(a) Function-like quasi_total Element of bool [:NAT,a:]
r . j is Element of a
F2 is Element of R
F1 . (F2,0) is Element of a
[F2,0] is V15() set
F1 . [F2,0] is set
F is Element of R
i is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
i + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
F1 . (F,(i + 1)) is Element of a
[F,(i + 1)] is V15() set
F1 . [F,(i + 1)] is set
F1 . (F,i) is Element of a
[F,i] is V15() set
F1 . [F,i] is set
n . ((F1 . (F,i)),F) is Element of a
[(F1 . (F,i)),F] is V15() set
n . [(F1 . (F,i)),F] is set
R is non empty left_zeroed addLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
<*a*> is V1() V4( NAT ) V5( the carrier of R) Function-like non empty trivial V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum <*a*> is Element of the carrier of R
[:NAT, the carrier of R:] is V35() set
bool [:NAT, the carrier of R:] is V35() set
len <*a*> is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
0. R is V54(R) Element of the carrier of R
n is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
n . (len <*a*>) is Element of the carrier of R
n . 0 is Element of the carrier of R
b is Element of the carrier of R
<*b*> is V1() V4( NAT ) V5( the carrier of R) Function-like non empty trivial V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len <*b*> is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
G1 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
<*a*> . (G1 + 1) is set
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
<*a*> . (0 + 1) is set
n . 1 is Element of the carrier of R
(0. R) + a is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((0. R),a) is Element of the carrier of R
[(0. R),a] is V15() set
the addF of R . [(0. R),a] is set
R is non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr
the carrier of R is non empty set
a is right_add-cancelable Element of the carrier of R
b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
a * b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (a * b) is right_add-cancelable Element of the carrier of R
Sum b is right_add-cancelable Element of the carrier of R
a * (Sum b) is right_add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . (a,(Sum b)) is right_add-cancelable Element of the carrier of R
[a,(Sum b)] is V15() set
the multF of R . [a,(Sum b)] is set
[:NAT, the carrier of R:] is V35() set
bool [:NAT, the carrier of R:] is V35() set
len b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
0. R is V54(R) right_add-cancelable Element of the carrier of R
n is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
n . (len b) is right_add-cancelable Element of the carrier of R
n . 0 is right_add-cancelable Element of the carrier of R
len (a * b) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
n . (len (a * b)) is right_add-cancelable Element of the carrier of R
n . 0 is right_add-cancelable Element of the carrier of R
Seg (len (a * b)) is V35() V42( len (a * b)) Element of bool NAT
dom (a * b) is Element of bool NAT
dom b is Element of bool NAT
Seg (len b) is V35() V42( len b) Element of bool NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n . G1 is right_add-cancelable Element of the carrier of R
a * (n . G1) is right_add-cancelable Element of the carrier of R
the multF of R . (a,(n . G1)) is right_add-cancelable Element of the carrier of R
[a,(n . G1)] is V15() set
the multF of R . [a,(n . G1)] is set
n . G1 is right_add-cancelable Element of the carrier of R
G1 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
n . (G1 + 1) is right_add-cancelable Element of the carrier of R
a * (n . (G1 + 1)) is right_add-cancelable Element of the carrier of R
the multF of R . (a,(n . (G1 + 1))) is right_add-cancelable Element of the carrier of R
[a,(n . (G1 + 1))] is V15() set
the multF of R . [a,(n . (G1 + 1))] is set
n . (G1 + 1) is right_add-cancelable Element of the carrier of R
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(a * b) /. (G1 + 1) is right_add-cancelable Element of the carrier of R
(a * b) . (G1 + 1) is set
b /. (G1 + 1) is right_add-cancelable Element of the carrier of R
b . (G1 + 1) is set
(a * (n . G1)) + ((a * b) /. (G1 + 1)) is right_add-cancelable Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the addF of R . ((a * (n . G1)),((a * b) /. (G1 + 1))) is right_add-cancelable Element of the carrier of R
[(a * (n . G1)),((a * b) /. (G1 + 1))] is V15() set
the addF of R . [(a * (n . G1)),((a * b) /. (G1 + 1))] is set
a * (b /. (G1 + 1)) is right_add-cancelable Element of the carrier of R
the multF of R . (a,(b /. (G1 + 1))) is right_add-cancelable Element of the carrier of R
[a,(b /. (G1 + 1))] is V15() set
the multF of R . [a,(b /. (G1 + 1))] is set
(a * (n . G1)) + (a * (b /. (G1 + 1))) is right_add-cancelable Element of the carrier of R
the addF of R . ((a * (n . G1)),(a * (b /. (G1 + 1)))) is right_add-cancelable Element of the carrier of R
[(a * (n . G1)),(a * (b /. (G1 + 1)))] is V15() set
the addF of R . [(a * (n . G1)),(a * (b /. (G1 + 1)))] is set
(n . G1) + (b /. (G1 + 1)) is right_add-cancelable Element of the carrier of R
the addF of R . ((n . G1),(b /. (G1 + 1))) is right_add-cancelable Element of the carrier of R
[(n . G1),(b /. (G1 + 1))] is V15() set
the addF of R . [(n . G1),(b /. (G1 + 1))] is set
a * ((n . G1) + (b /. (G1 + 1))) is right_add-cancelable Element of the carrier of R
the multF of R . (a,((n . G1) + (b /. (G1 + 1)))) is right_add-cancelable Element of the carrier of R
[a,((n . G1) + (b /. (G1 + 1)))] is V15() set
the multF of R . [a,((n . G1) + (b /. (G1 + 1)))] is set
a * (n . 0) is right_add-cancelable Element of the carrier of R
the multF of R . (a,(n . 0)) is right_add-cancelable Element of the carrier of R
[a,(n . 0)] is V15() set
the multF of R . [a,(n . 0)] is set
n . (len b) is right_add-cancelable Element of the carrier of R
R is non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr
the carrier of R is non empty set
a is left_add-cancelable Element of the carrier of R
b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
b * a is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (b * a) is left_add-cancelable Element of the carrier of R
Sum b is left_add-cancelable Element of the carrier of R
(Sum b) * a is left_add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((Sum b),a) is left_add-cancelable Element of the carrier of R
[(Sum b),a] is V15() set
the multF of R . [(Sum b),a] is set
[:NAT, the carrier of R:] is V35() set
bool [:NAT, the carrier of R:] is V35() set
len b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
0. R is V54(R) left_add-cancelable Element of the carrier of R
n is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
n . (len b) is left_add-cancelable Element of the carrier of R
n . 0 is left_add-cancelable Element of the carrier of R
len (b * a) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
n . (len (b * a)) is left_add-cancelable Element of the carrier of R
n . 0 is left_add-cancelable Element of the carrier of R
Seg (len (b * a)) is V35() V42( len (b * a)) Element of bool NAT
dom (b * a) is Element of bool NAT
dom b is Element of bool NAT
Seg (len b) is V35() V42( len b) Element of bool NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n . G1 is left_add-cancelable Element of the carrier of R
(n . G1) * a is left_add-cancelable Element of the carrier of R
the multF of R . ((n . G1),a) is left_add-cancelable Element of the carrier of R
[(n . G1),a] is V15() set
the multF of R . [(n . G1),a] is set
n . G1 is left_add-cancelable Element of the carrier of R
G1 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
n . (G1 + 1) is left_add-cancelable Element of the carrier of R
(n . (G1 + 1)) * a is left_add-cancelable Element of the carrier of R
the multF of R . ((n . (G1 + 1)),a) is left_add-cancelable Element of the carrier of R
[(n . (G1 + 1)),a] is V15() set
the multF of R . [(n . (G1 + 1)),a] is set
n . (G1 + 1) is left_add-cancelable Element of the carrier of R
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(b * a) /. (G1 + 1) is left_add-cancelable Element of the carrier of R
(b * a) . (G1 + 1) is set
b /. (G1 + 1) is left_add-cancelable Element of the carrier of R
b . (G1 + 1) is set
((n . G1) * a) + ((b * a) /. (G1 + 1)) is left_add-cancelable Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the addF of R . (((n . G1) * a),((b * a) /. (G1 + 1))) is left_add-cancelable Element of the carrier of R
[((n . G1) * a),((b * a) /. (G1 + 1))] is V15() set
the addF of R . [((n . G1) * a),((b * a) /. (G1 + 1))] is set
(b /. (G1 + 1)) * a is left_add-cancelable Element of the carrier of R
the multF of R . ((b /. (G1 + 1)),a) is left_add-cancelable Element of the carrier of R
[(b /. (G1 + 1)),a] is V15() set
the multF of R . [(b /. (G1 + 1)),a] is set
((n . G1) * a) + ((b /. (G1 + 1)) * a) is left_add-cancelable Element of the carrier of R
the addF of R . (((n . G1) * a),((b /. (G1 + 1)) * a)) is left_add-cancelable Element of the carrier of R
[((n . G1) * a),((b /. (G1 + 1)) * a)] is V15() set
the addF of R . [((n . G1) * a),((b /. (G1 + 1)) * a)] is set
(n . G1) + (b /. (G1 + 1)) is left_add-cancelable Element of the carrier of R
the addF of R . ((n . G1),(b /. (G1 + 1))) is left_add-cancelable Element of the carrier of R
[(n . G1),(b /. (G1 + 1))] is V15() set
the addF of R . [(n . G1),(b /. (G1 + 1))] is set
((n . G1) + (b /. (G1 + 1))) * a is left_add-cancelable Element of the carrier of R
the multF of R . (((n . G1) + (b /. (G1 + 1))),a) is left_add-cancelable Element of the carrier of R
[((n . G1) + (b /. (G1 + 1))),a] is V15() set
the multF of R . [((n . G1) + (b /. (G1 + 1))),a] is set
(n . 0) * a is left_add-cancelable Element of the carrier of R
the multF of R . ((n . 0),a) is left_add-cancelable Element of the carrier of R
[(n . 0),a] is V15() set
the multF of R . [(n . 0),a] is set
n . (len b) is left_add-cancelable Element of the carrier of R
R is non empty commutative multMagma
the carrier of R is non empty set
a is Element of the carrier of R
b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
b * a is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
a * b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom (b * a) is Element of bool NAT
dom b is Element of bool NAT
dom (a * b) is Element of bool NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(b * a) /. G1 is Element of the carrier of R
b /. G1 is Element of the carrier of R
(b /. G1) * a is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((b /. G1),a) is Element of the carrier of R
[(b /. G1),a] is V15() set
the multF of R . [(b /. G1),a] is set
(a * b) /. G1 is Element of the carrier of R
R is non empty addLoopStr
the carrier of R is non empty set
a is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom a is Element of bool NAT
b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len a is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
Seg (len a) is V35() V42( len a) Element of bool NAT
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
a /. n is Element of the carrier of R
b /. n is Element of the carrier of R
(a /. n) + (b /. n) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((a /. n),(b /. n)) is Element of the carrier of R
[(a /. n),(b /. n)] is V15() set
the addF of R . [(a /. n),(b /. n)] is set
n is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom n is Element of bool NAT
len n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
n /. n is Element of the carrier of R
a /. n is Element of the carrier of R
b /. n is Element of the carrier of R
(a /. n) + (b /. n) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((a /. n),(b /. n)) is Element of the carrier of R
[(a /. n),(b /. n)] is V15() set
the addF of R . [(a /. n),(b /. n)] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
n /. n is Element of the carrier of R
a /. n is Element of the carrier of R
b /. n is Element of the carrier of R
(a /. n) + (b /. n) is Element of the carrier of R
the addF of R . ((a /. n),(b /. n)) is Element of the carrier of R
[(a /. n),(b /. n)] is V15() set
the addF of R . [(a /. n),(b /. n)] is set
n is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom n is Element of bool NAT
len n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom n is Element of bool NAT
len n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
Seg (len n) is V35() V42( len n) Element of bool NAT
Seg (len n) is V35() V42( len n) Element of bool NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
n . G1 is set
n /. G1 is Element of the carrier of R
a /. G1 is Element of the carrier of R
b /. G1 is Element of the carrier of R
(a /. G1) + (b /. G1) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((a /. G1),(b /. G1)) is Element of the carrier of R
[(a /. G1),(b /. G1)] is V15() set
the addF of R . [(a /. G1),(b /. G1)] is set
n /. G1 is Element of the carrier of R
n . G1 is set
R is non empty Abelian add-associative right_zeroed addLoopStr
the carrier of R is non empty set
a is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom a is Element of bool NAT
b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom b is Element of bool NAT
(R,a,b) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,a,b) is Element of the carrier of R
Sum a is Element of the carrier of R
Sum b is Element of the carrier of R
(Sum a) + (Sum b) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((Sum a),(Sum b)) is Element of the carrier of R
[(Sum a),(Sum b)] is V15() set
the addF of R . [(Sum a),(Sum b)] is set
[:NAT, the carrier of R:] is V35() set
bool [:NAT, the carrier of R:] is V35() set
len a is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
0. R is V54(R) Element of the carrier of R
n is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
n . (len a) is Element of the carrier of R
n . 0 is Element of the carrier of R
len b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
n . (len b) is Element of the carrier of R
n . 0 is Element of the carrier of R
Seg (len a) is V35() V42( len a) Element of bool NAT
Seg (len b) is V35() V42( len b) Element of bool NAT
len (R,a,b) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
G1 is V1() V4( NAT ) V5( the carrier of R) Function-like quasi_total Element of bool [:NAT, the carrier of R:]
G1 . (len (R,a,b)) is Element of the carrier of R
G1 . 0 is Element of the carrier of R
dom (R,a,b) is Element of bool NAT
Seg (len (R,a,b)) is V35() V42( len (R,a,b)) Element of bool NAT
G2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n . G2 is Element of the carrier of R
n . G2 is Element of the carrier of R
(n . G2) + (n . G2) is Element of the carrier of R
the addF of R . ((n . G2),(n . G2)) is Element of the carrier of R
[(n . G2),(n . G2)] is V15() set
the addF of R . [(n . G2),(n . G2)] is set
G1 . G2 is Element of the carrier of R
G2 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
n . (G2 + 1) is Element of the carrier of R
n . (G2 + 1) is Element of the carrier of R
(n . (G2 + 1)) + (n . (G2 + 1)) is Element of the carrier of R
the addF of R . ((n . (G2 + 1)),(n . (G2 + 1))) is Element of the carrier of R
[(n . (G2 + 1)),(n . (G2 + 1))] is V15() set
the addF of R . [(n . (G2 + 1)),(n . (G2 + 1))] is set
G1 . (G2 + 1) is Element of the carrier of R
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
a /. (G2 + 1) is Element of the carrier of R
a . (G2 + 1) is set
b /. (G2 + 1) is Element of the carrier of R
b . (G2 + 1) is set
(R,a,b) /. (G2 + 1) is Element of the carrier of R
(R,a,b) . (G2 + 1) is set
(G1 . G2) + ((R,a,b) /. (G2 + 1)) is Element of the carrier of R
the addF of R . ((G1 . G2),((R,a,b) /. (G2 + 1))) is Element of the carrier of R
[(G1 . G2),((R,a,b) /. (G2 + 1))] is V15() set
the addF of R . [(G1 . G2),((R,a,b) /. (G2 + 1))] is set
(a /. (G2 + 1)) + (b /. (G2 + 1)) is Element of the carrier of R
the addF of R . ((a /. (G2 + 1)),(b /. (G2 + 1))) is Element of the carrier of R
[(a /. (G2 + 1)),(b /. (G2 + 1))] is V15() set
the addF of R . [(a /. (G2 + 1)),(b /. (G2 + 1))] is set
((n . G2) + (n . G2)) + ((a /. (G2 + 1)) + (b /. (G2 + 1))) is Element of the carrier of R
the addF of R . (((n . G2) + (n . G2)),((a /. (G2 + 1)) + (b /. (G2 + 1)))) is Element of the carrier of R
[((n . G2) + (n . G2)),((a /. (G2 + 1)) + (b /. (G2 + 1)))] is V15() set
the addF of R . [((n . G2) + (n . G2)),((a /. (G2 + 1)) + (b /. (G2 + 1)))] is set
(n . G2) + ((a /. (G2 + 1)) + (b /. (G2 + 1))) is Element of the carrier of R
the addF of R . ((n . G2),((a /. (G2 + 1)) + (b /. (G2 + 1)))) is Element of the carrier of R
[(n . G2),((a /. (G2 + 1)) + (b /. (G2 + 1)))] is V15() set
the addF of R . [(n . G2),((a /. (G2 + 1)) + (b /. (G2 + 1)))] is set
(n . G2) + ((n . G2) + ((a /. (G2 + 1)) + (b /. (G2 + 1)))) is Element of the carrier of R
the addF of R . ((n . G2),((n . G2) + ((a /. (G2 + 1)) + (b /. (G2 + 1))))) is Element of the carrier of R
[(n . G2),((n . G2) + ((a /. (G2 + 1)) + (b /. (G2 + 1))))] is V15() set
the addF of R . [(n . G2),((n . G2) + ((a /. (G2 + 1)) + (b /. (G2 + 1))))] is set
(n . G2) + (b /. (G2 + 1)) is Element of the carrier of R
the addF of R . ((n . G2),(b /. (G2 + 1))) is Element of the carrier of R
[(n . G2),(b /. (G2 + 1))] is V15() set
the addF of R . [(n . G2),(b /. (G2 + 1))] is set
(a /. (G2 + 1)) + ((n . G2) + (b /. (G2 + 1))) is Element of the carrier of R
the addF of R . ((a /. (G2 + 1)),((n . G2) + (b /. (G2 + 1)))) is Element of the carrier of R
[(a /. (G2 + 1)),((n . G2) + (b /. (G2 + 1)))] is V15() set
the addF of R . [(a /. (G2 + 1)),((n . G2) + (b /. (G2 + 1)))] is set
(n . G2) + ((a /. (G2 + 1)) + ((n . G2) + (b /. (G2 + 1)))) is Element of the carrier of R
the addF of R . ((n . G2),((a /. (G2 + 1)) + ((n . G2) + (b /. (G2 + 1))))) is Element of the carrier of R
[(n . G2),((a /. (G2 + 1)) + ((n . G2) + (b /. (G2 + 1))))] is V15() set
the addF of R . [(n . G2),((a /. (G2 + 1)) + ((n . G2) + (b /. (G2 + 1))))] is set
(n . G2) + (a /. (G2 + 1)) is Element of the carrier of R
the addF of R . ((n . G2),(a /. (G2 + 1))) is Element of the carrier of R
[(n . G2),(a /. (G2 + 1))] is V15() set
the addF of R . [(n . G2),(a /. (G2 + 1))] is set
((n . G2) + (a /. (G2 + 1))) + ((n . G2) + (b /. (G2 + 1))) is Element of the carrier of R
the addF of R . (((n . G2) + (a /. (G2 + 1))),((n . G2) + (b /. (G2 + 1)))) is Element of the carrier of R
[((n . G2) + (a /. (G2 + 1))),((n . G2) + (b /. (G2 + 1)))] is V15() set
the addF of R . [((n . G2) + (a /. (G2 + 1))),((n . G2) + (b /. (G2 + 1)))] is set
(n . (G2 + 1)) + ((n . G2) + (b /. (G2 + 1))) is Element of the carrier of R
the addF of R . ((n . (G2 + 1)),((n . G2) + (b /. (G2 + 1)))) is Element of the carrier of R
[(n . (G2 + 1)),((n . G2) + (b /. (G2 + 1)))] is V15() set
the addF of R . [(n . (G2 + 1)),((n . G2) + (b /. (G2 + 1)))] is set
(n . 0) + (n . 0) is Element of the carrier of R
the addF of R . ((n . 0),(n . 0)) is Element of the carrier of R
[(n . 0),(n . 0)] is V15() set
the addF of R . [(n . 0),(n . 0)] is set
G1 . (len a) is Element of the carrier of R
R is non empty unital multMagma
the carrier of R is non empty set
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(power R) . (a,b) is set
[a,b] is V15() set
(power R) . [a,b] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(power R) . (a,n) is Element of the carrier of R
[a,n] is V15() set
(power R) . [a,n] is set
R is non empty unital multMagma
the carrier of R is non empty set
1_ R is Element of the carrier of R
a is Element of the carrier of R
(R,a,0) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,0) is set
[a,0] is V15() set
(power R) . [a,0] is set
(R,a,1) is Element of the carrier of R
(power R) . (a,1) is set
[a,1] is V15() set
(power R) . [a,1] is set
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(power R) . (a,1) is Element of the carrier of R
(power R) . (a,0) is Element of the carrier of R
((power R) . (a,0)) * a is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . (((power R) . (a,0)),a) is Element of the carrier of R
[((power R) . (a,0)),a] is V15() set
the multF of R . [((power R) . (a,0)),a] is set
(1_ R) * a is Element of the carrier of R
the multF of R . ((1_ R),a) is Element of the carrier of R
[(1_ R),a] is V15() set
the multF of R . [(1_ R),a] is set
R is non empty unital associative commutative multMagma
the carrier of R is non empty set
a is Element of the carrier of R
b is Element of the carrier of R
a * b is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . (a,b) is Element of the carrier of R
[a,b] is V15() set
the multF of R . [a,b] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(R,(a * b),n) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . ((a * b),n) is set
[(a * b),n] is V15() set
(power R) . [(a * b),n] is set
(R,a,n) is Element of the carrier of R
(power R) . (a,n) is set
[a,n] is V15() set
(power R) . [a,n] is set
(R,b,n) is Element of the carrier of R
(power R) . (b,n) is set
[b,n] is V15() set
(power R) . [b,n] is set
(R,a,n) * (R,b,n) is Element of the carrier of R
the multF of R . ((R,a,n),(R,b,n)) is Element of the carrier of R
[(R,a,n),(R,b,n)] is V15() set
the multF of R . [(R,a,n),(R,b,n)] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(power R) . ((a * b),n) is Element of the carrier of R
[(a * b),n] is V15() set
(power R) . [(a * b),n] is set
(power R) . (a,n) is Element of the carrier of R
[a,n] is V15() set
(power R) . [a,n] is set
(power R) . (b,n) is Element of the carrier of R
[b,n] is V15() set
(power R) . [b,n] is set
((power R) . (a,n)) * ((power R) . (b,n)) is Element of the carrier of R
the multF of R . (((power R) . (a,n)),((power R) . (b,n))) is Element of the carrier of R
[((power R) . (a,n)),((power R) . (b,n))] is V15() set
the multF of R . [((power R) . (a,n)),((power R) . (b,n))] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(power R) . ((a * b),(n + 1)) is Element of the carrier of R
[(a * b),(n + 1)] is V15() set
(power R) . [(a * b),(n + 1)] is set
(((power R) . (a,n)) * ((power R) . (b,n))) * (a * b) is Element of the carrier of R
the multF of R . ((((power R) . (a,n)) * ((power R) . (b,n))),(a * b)) is Element of the carrier of R
[(((power R) . (a,n)) * ((power R) . (b,n))),(a * b)] is V15() set
the multF of R . [(((power R) . (a,n)) * ((power R) . (b,n))),(a * b)] is set
(((power R) . (a,n)) * ((power R) . (b,n))) * a is Element of the carrier of R
the multF of R . ((((power R) . (a,n)) * ((power R) . (b,n))),a) is Element of the carrier of R
[(((power R) . (a,n)) * ((power R) . (b,n))),a] is V15() set
the multF of R . [(((power R) . (a,n)) * ((power R) . (b,n))),a] is set
((((power R) . (a,n)) * ((power R) . (b,n))) * a) * b is Element of the carrier of R
the multF of R . (((((power R) . (a,n)) * ((power R) . (b,n))) * a),b) is Element of the carrier of R
[((((power R) . (a,n)) * ((power R) . (b,n))) * a),b] is V15() set
the multF of R . [((((power R) . (a,n)) * ((power R) . (b,n))) * a),b] is set
((power R) . (a,n)) * a is Element of the carrier of R
the multF of R . (((power R) . (a,n)),a) is Element of the carrier of R
[((power R) . (a,n)),a] is V15() set
the multF of R . [((power R) . (a,n)),a] is set
(((power R) . (a,n)) * a) * ((power R) . (b,n)) is Element of the carrier of R
the multF of R . ((((power R) . (a,n)) * a),((power R) . (b,n))) is Element of the carrier of R
[(((power R) . (a,n)) * a),((power R) . (b,n))] is V15() set
the multF of R . [(((power R) . (a,n)) * a),((power R) . (b,n))] is set
((((power R) . (a,n)) * a) * ((power R) . (b,n))) * b is Element of the carrier of R
the multF of R . (((((power R) . (a,n)) * a) * ((power R) . (b,n))),b) is Element of the carrier of R
[((((power R) . (a,n)) * a) * ((power R) . (b,n))),b] is V15() set
the multF of R . [((((power R) . (a,n)) * a) * ((power R) . (b,n))),b] is set
((power R) . (b,n)) * b is Element of the carrier of R
the multF of R . (((power R) . (b,n)),b) is Element of the carrier of R
[((power R) . (b,n)),b] is V15() set
the multF of R . [((power R) . (b,n)),b] is set
(((power R) . (a,n)) * a) * (((power R) . (b,n)) * b) is Element of the carrier of R
the multF of R . ((((power R) . (a,n)) * a),(((power R) . (b,n)) * b)) is Element of the carrier of R
[(((power R) . (a,n)) * a),(((power R) . (b,n)) * b)] is V15() set
the multF of R . [(((power R) . (a,n)) * a),(((power R) . (b,n)) * b)] is set
(power R) . (a,(n + 1)) is Element of the carrier of R
[a,(n + 1)] is V15() set
(power R) . [a,(n + 1)] is set
((power R) . (a,(n + 1))) * (((power R) . (b,n)) * b) is Element of the carrier of R
the multF of R . (((power R) . (a,(n + 1))),(((power R) . (b,n)) * b)) is Element of the carrier of R
[((power R) . (a,(n + 1))),(((power R) . (b,n)) * b)] is V15() set
the multF of R . [((power R) . (a,(n + 1))),(((power R) . (b,n)) * b)] is set
(power R) . (b,(n + 1)) is Element of the carrier of R
[b,(n + 1)] is V15() set
(power R) . [b,(n + 1)] is set
((power R) . (a,(n + 1))) * ((power R) . (b,(n + 1))) is Element of the carrier of R
the multF of R . (((power R) . (a,(n + 1))),((power R) . (b,(n + 1)))) is Element of the carrier of R
[((power R) . (a,(n + 1))),((power R) . (b,(n + 1)))] is V15() set
the multF of R . [((power R) . (a,(n + 1))),((power R) . (b,(n + 1)))] is set
(power R) . ((a * b),0) is Element of the carrier of R
[(a * b),0] is V15() set
(power R) . [(a * b),0] is set
1_ R is Element of the carrier of R
(1_ R) * (1_ R) is Element of the carrier of R
the multF of R . ((1_ R),(1_ R)) is Element of the carrier of R
[(1_ R),(1_ R)] is V15() set
the multF of R . [(1_ R),(1_ R)] is set
(power R) . (a,0) is Element of the carrier of R
[a,0] is V15() set
(power R) . [a,0] is set
((power R) . (a,0)) * (1_ R) is Element of the carrier of R
the multF of R . (((power R) . (a,0)),(1_ R)) is Element of the carrier of R
[((power R) . (a,0)),(1_ R)] is V15() set
the multF of R . [((power R) . (a,0)),(1_ R)] is set
(power R) . (b,0) is Element of the carrier of R
[b,0] is V15() set
(power R) . [b,0] is set
((power R) . (a,0)) * ((power R) . (b,0)) is Element of the carrier of R
the multF of R . (((power R) . (a,0)),((power R) . (b,0))) is Element of the carrier of R
[((power R) . (a,0)),((power R) . (b,0))] is V15() set
the multF of R . [((power R) . (a,0)),((power R) . (b,0))] is set
R is non empty unital associative multMagma
the carrier of R is non empty set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
b + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(b + n)) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,(b + n)) is set
[a,(b + n)] is V15() set
(power R) . [a,(b + n)] is set
(R,a,b) is Element of the carrier of R
(power R) . (a,b) is set
[a,b] is V15() set
(power R) . [a,b] is set
(R,a,n) is Element of the carrier of R
(power R) . (a,n) is set
[a,n] is V15() set
(power R) . [a,n] is set
(R,a,b) * (R,a,n) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,a,b),(R,a,n)) is Element of the carrier of R
[(R,a,b),(R,a,n)] is V15() set
the multF of R . [(R,a,b),(R,a,n)] is set
(power R) . (a,b) is Element of the carrier of R
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
b + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(power R) . (a,(b + n)) is Element of the carrier of R
[a,(b + n)] is V15() set
(power R) . [a,(b + n)] is set
(power R) . (a,n) is Element of the carrier of R
[a,n] is V15() set
(power R) . [a,n] is set
((power R) . (a,b)) * ((power R) . (a,n)) is Element of the carrier of R
the multF of R . (((power R) . (a,b)),((power R) . (a,n))) is Element of the carrier of R
[((power R) . (a,b)),((power R) . (a,n))] is V15() set
the multF of R . [((power R) . (a,b)),((power R) . (a,n))] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
b + (n + 1) is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(power R) . (a,(b + (n + 1))) is Element of the carrier of R
[a,(b + (n + 1))] is V15() set
(power R) . [a,(b + (n + 1))] is set
(b + n) + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(power R) . (a,((b + n) + 1)) is Element of the carrier of R
[a,((b + n) + 1)] is V15() set
(power R) . [a,((b + n) + 1)] is set
(((power R) . (a,b)) * ((power R) . (a,n))) * a is Element of the carrier of R
the multF of R . ((((power R) . (a,b)) * ((power R) . (a,n))),a) is Element of the carrier of R
[(((power R) . (a,b)) * ((power R) . (a,n))),a] is V15() set
the multF of R . [(((power R) . (a,b)) * ((power R) . (a,n))),a] is set
((power R) . (a,n)) * a is Element of the carrier of R
the multF of R . (((power R) . (a,n)),a) is Element of the carrier of R
[((power R) . (a,n)),a] is V15() set
the multF of R . [((power R) . (a,n)),a] is set
((power R) . (a,b)) * (((power R) . (a,n)) * a) is Element of the carrier of R
the multF of R . (((power R) . (a,b)),(((power R) . (a,n)) * a)) is Element of the carrier of R
[((power R) . (a,b)),(((power R) . (a,n)) * a)] is V15() set
the multF of R . [((power R) . (a,b)),(((power R) . (a,n)) * a)] is set
(power R) . (a,(n + 1)) is Element of the carrier of R
[a,(n + 1)] is V15() set
(power R) . [a,(n + 1)] is set
((power R) . (a,b)) * ((power R) . (a,(n + 1))) is Element of the carrier of R
the multF of R . (((power R) . (a,b)),((power R) . (a,(n + 1)))) is Element of the carrier of R
[((power R) . (a,b)),((power R) . (a,(n + 1)))] is V15() set
the multF of R . [((power R) . (a,b)),((power R) . (a,(n + 1)))] is set
b + 0 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(power R) . (a,(b + 0)) is Element of the carrier of R
[a,(b + 0)] is V15() set
(power R) . [a,(b + 0)] is set
1_ R is Element of the carrier of R
((power R) . (a,b)) * (1_ R) is Element of the carrier of R
the multF of R . (((power R) . (a,b)),(1_ R)) is Element of the carrier of R
[((power R) . (a,b)),(1_ R)] is V15() set
the multF of R . [((power R) . (a,b)),(1_ R)] is set
(power R) . (a,0) is Element of the carrier of R
[a,0] is V15() set
(power R) . [a,0] is set
((power R) . (a,b)) * ((power R) . (a,0)) is Element of the carrier of R
the multF of R . (((power R) . (a,b)),((power R) . (a,0))) is Element of the carrier of R
[((power R) . (a,b)),((power R) . (a,0))] is V15() set
the multF of R . [((power R) . (a,b)),((power R) . (a,0))] is set
R is non empty unital associative multMagma
the carrier of R is non empty set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
b + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(R,a,(b + n)) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,(b + n)) is set
[a,(b + n)] is V15() set
(power R) . [a,(b + n)] is set
(R,a,b) is Element of the carrier of R
(power R) . (a,b) is set
[a,b] is V15() set
(power R) . [a,b] is set
(R,a,n) is Element of the carrier of R
(power R) . (a,n) is set
[a,n] is V15() set
(power R) . [a,n] is set
(R,a,b) * (R,a,n) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,a,b),(R,a,n)) is Element of the carrier of R
[(R,a,b),(R,a,n)] is V15() set
the multF of R . [(R,a,b),(R,a,n)] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n + G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(n + G1)) is Element of the carrier of R
(power R) . (a,(n + G1)) is set
[a,(n + G1)] is V15() set
(power R) . [a,(n + G1)] is set
(R,a,n) is Element of the carrier of R
(power R) . (a,n) is set
[a,n] is V15() set
(power R) . [a,n] is set
(R,a,G1) is Element of the carrier of R
(power R) . (a,G1) is set
[a,G1] is V15() set
(power R) . [a,G1] is set
(R,a,n) * (R,a,G1) is Element of the carrier of R
the multF of R . ((R,a,n),(R,a,G1)) is Element of the carrier of R
[(R,a,n),(R,a,G1)] is V15() set
the multF of R . [(R,a,n),(R,a,G1)] is set
R is non empty unital associative multMagma
the carrier of R is non empty set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(R,a,b) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,b) is set
[a,b] is V15() set
(power R) . [a,b] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(R,(R,a,b),n) is Element of the carrier of R
(power R) . ((R,a,b),n) is set
[(R,a,b),n] is V15() set
(power R) . [(R,a,b),n] is set
b * n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(R,a,(b * n)) is Element of the carrier of R
(power R) . (a,(b * n)) is set
[a,(b * n)] is V15() set
(power R) . [a,(b * n)] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(power R) . ((R,a,b),n) is Element of the carrier of R
[(R,a,b),n] is V15() set
(power R) . [(R,a,b),n] is set
b * n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(power R) . (a,(b * n)) is Element of the carrier of R
[a,(b * n)] is V15() set
(power R) . [a,(b * n)] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(power R) . ((R,a,b),(n + 1)) is Element of the carrier of R
[(R,a,b),(n + 1)] is V15() set
(power R) . [(R,a,b),(n + 1)] is set
(R,a,(b * n)) is Element of the carrier of R
(power R) . (a,(b * n)) is set
(R,a,(b * n)) * (R,a,b) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,a,(b * n)),(R,a,b)) is Element of the carrier of R
[(R,a,(b * n)),(R,a,b)] is V15() set
the multF of R . [(R,a,(b * n)),(R,a,b)] is set
(b * n) + b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,((b * n) + b)) is Element of the carrier of R
(power R) . (a,((b * n) + b)) is set
[a,((b * n) + b)] is V15() set
(power R) . [a,((b * n) + b)] is set
b * (n + 1) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(power R) . (a,(b * (n + 1))) is Element of the carrier of R
[a,(b * (n + 1))] is V15() set
(power R) . [a,(b * (n + 1))] is set
(power R) . ((R,a,b),0) is Element of the carrier of R
[(R,a,b),0] is V15() set
(power R) . [(R,a,b),0] is set
1_ R is Element of the carrier of R
b * 0 is functional empty V24() V25() V26() V28() V29() V30() V31() V32() V33() V35() V40() V42( {} ) FinSequence-membered ext-real non positive non negative Element of NAT
(power R) . (a,(b * 0)) is Element of the carrier of R
[a,(b * 0)] is V15() set
(power R) . [a,(b * 0)] is set
R is non empty addLoopStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
0. R is V54(R) Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
b is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
n is Element of the carrier of R
b . (0,n) is Element of the carrier of R
[0,n] is V15() set
b . [0,n] is set
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
G1 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
n is Element of the carrier of R
b . ((G1 + 1),n) is Element of the carrier of R
[(G1 + 1),n] is V15() set
b . [(G1 + 1),n] is set
b . (G1,n) is Element of the carrier of R
[G1,n] is V15() set
b . [G1,n] is set
n + (b . (G1,n)) is Element of the carrier of R
the addF of R . (n,(b . (G1,n))) is Element of the carrier of R
[n,(b . (G1,n))] is V15() set
the addF of R . [n,(b . (G1,n))] is set
a is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
b is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
n is Element of the carrier of R
a . ((n + 1),n) is Element of the carrier of R
[(n + 1),n] is V15() set
a . [(n + 1),n] is set
a . (n,n) is Element of the carrier of R
[n,n] is V15() set
a . [n,n] is set
n + (a . (n,n)) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . (n,(a . (n,n))) is Element of the carrier of R
[n,(a . (n,n))] is V15() set
the addF of R . [n,(a . (n,n))] is set
b . (n,n) is Element of the carrier of R
b . [n,n] is set
n + (b . (n,n)) is Element of the carrier of R
the addF of R . (n,(b . (n,n))) is Element of the carrier of R
[n,(b . (n,n))] is V15() set
the addF of R . [n,(b . (n,n))] is set
b . ((n + 1),n) is Element of the carrier of R
b . [(n + 1),n] is set
n is Element of the carrier of R
a . ((n + 1),n) is Element of the carrier of R
[(n + 1),n] is V15() set
a . [(n + 1),n] is set
b . ((n + 1),n) is Element of the carrier of R
b . [(n + 1),n] is set
n is Element of the carrier of R
a . (0,n) is Element of the carrier of R
[0,n] is V15() set
a . [0,n] is set
b . (0,n) is Element of the carrier of R
b . [0,n] is set
n is set
n is set
G1 is set
[n,G1] is V15() set
a . n is set
F1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
G2 is Element of the carrier of R
a . (F1,G2) is Element of the carrier of R
[F1,G2] is V15() set
a . [F1,G2] is set
b . (F1,G2) is Element of the carrier of R
b . [F1,G2] is set
b . n is set
dom a is V1() V4( NAT ) V5( the carrier of R) Element of bool [:NAT, the carrier of R:]
bool [:NAT, the carrier of R:] is V35() set
dom b is V1() V4( NAT ) V5( the carrier of R) Element of bool [:NAT, the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
a is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
b is Element of the carrier of R
a . (b,0) is Element of the carrier of R
[b,0] is V15() set
a . [b,0] is set
n is Element of the carrier of R
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
a . (n,(n + 1)) is Element of the carrier of R
[n,(n + 1)] is V15() set
a . [n,(n + 1)] is set
a . (n,n) is Element of the carrier of R
[n,n] is V15() set
a . [n,n] is set
(a . (n,n)) + n is Element of the carrier of R
the addF of R . ((a . (n,n)),n) is Element of the carrier of R
[(a . (n,n)),n] is V15() set
the addF of R . [(a . (n,n)),n] is set
a is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
b is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is Element of the carrier of R
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
a . (n,(n + 1)) is Element of the carrier of R
[n,(n + 1)] is V15() set
a . [n,(n + 1)] is set
a . (n,n) is Element of the carrier of R
[n,n] is V15() set
a . [n,n] is set
(a . (n,n)) + n is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((a . (n,n)),n) is Element of the carrier of R
[(a . (n,n)),n] is V15() set
the addF of R . [(a . (n,n)),n] is set
b . (n,n) is Element of the carrier of R
b . [n,n] is set
(b . (n,n)) + n is Element of the carrier of R
the addF of R . ((b . (n,n)),n) is Element of the carrier of R
[(b . (n,n)),n] is V15() set
the addF of R . [(b . (n,n)),n] is set
b . (n,(n + 1)) is Element of the carrier of R
b . [n,(n + 1)] is set
n is Element of the carrier of R
a . (n,(n + 1)) is Element of the carrier of R
[n,(n + 1)] is V15() set
a . [n,(n + 1)] is set
b . (n,(n + 1)) is Element of the carrier of R
b . [n,(n + 1)] is set
n is Element of the carrier of R
a . (n,0) is Element of the carrier of R
[n,0] is V15() set
a . [n,0] is set
b . (n,0) is Element of the carrier of R
b . [n,0] is set
n is set
n is set
G1 is set
[n,G1] is V15() set
a . n is set
G2 is Element of the carrier of R
F1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
a . (G2,F1) is Element of the carrier of R
[G2,F1] is V15() set
a . [G2,F1] is set
b . (G2,F1) is Element of the carrier of R
b . [G2,F1] is set
b . n is set
dom a is V1() V4( the carrier of R) V5( NAT ) Element of bool [: the carrier of R,NAT:]
bool [: the carrier of R,NAT:] is V35() set
dom b is V1() V4( the carrier of R) V5( NAT ) Element of bool [: the carrier of R,NAT:]
R is non empty addLoopStr
the carrier of R is non empty set
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
a is Element of the carrier of R
(R) . (b,a) is Element of the carrier of R
[b,a] is V15() set
(R) . [b,a] is set
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(R) . (a,b) is Element of the carrier of R
[a,b] is V15() set
(R) . [a,b] is set
R is non empty addLoopStr
the carrier of R is non empty set
b is non empty addLoopStr
the carrier of b is non empty set
a is Element of the carrier of R
(R,a,0) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . (0,a) is Element of the carrier of R
[0,a] is V15() set
(R) . [0,a] is set
0. R is V54(R) Element of the carrier of R
n is Element of the carrier of b
(b,n,0) is Element of the carrier of b
(b) is V1() V4([: the carrier of b,NAT:]) V5( the carrier of b) Function-like quasi_total Element of bool [:[: the carrier of b,NAT:], the carrier of b:]
[: the carrier of b,NAT:] is V35() set
[:[: the carrier of b,NAT:], the carrier of b:] is V35() set
bool [:[: the carrier of b,NAT:], the carrier of b:] is V35() set
(b) . (n,0) is Element of the carrier of b
[n,0] is V15() set
(b) . [n,0] is set
0. b is V54(b) Element of the carrier of b
R is non empty right_zeroed addLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
(R,a,1) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . (1,a) is Element of the carrier of R
[1,a] is V15() set
(R) . [1,a] is set
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R) . ((0 + 1),a) is Element of the carrier of R
[(0 + 1),a] is V15() set
(R) . [(0 + 1),a] is set
(R) . (0,a) is Element of the carrier of R
[0,a] is V15() set
(R) . [0,a] is set
a + ((R) . (0,a)) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . (a,((R) . (0,a))) is Element of the carrier of R
[a,((R) . (0,a))] is V15() set
the addF of R . [a,((R) . (0,a))] is set
0. R is V54(R) Element of the carrier of R
a + (0. R) is Element of the carrier of R
the addF of R . (a,(0. R)) is Element of the carrier of R
[a,(0. R)] is V15() set
the addF of R . [a,(0. R)] is set
R is non empty left_zeroed addLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
(R,a,1) is Element of the carrier of R
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(R) . (a,1) is Element of the carrier of R
[a,1] is V15() set
(R) . [a,1] is set
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R) . (a,(0 + 1)) is Element of the carrier of R
[a,(0 + 1)] is V15() set
(R) . [a,(0 + 1)] is set
(R) . (a,0) is Element of the carrier of R
[a,0] is V15() set
(R) . [a,0] is set
((R) . (a,0)) + a is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . (((R) . (a,0)),a) is Element of the carrier of R
[((R) . (a,0)),a] is V15() set
the addF of R . [((R) . (a,0)),a] is set
0. R is V54(R) Element of the carrier of R
(0. R) + a is Element of the carrier of R
the addF of R . ((0. R),a) is Element of the carrier of R
[(0. R),a] is V15() set
the addF of R . [(0. R),a] is set
R is non empty left_zeroed add-associative addLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
b + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(b + n)) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . ((b + n),a) is Element of the carrier of R
[(b + n),a] is V15() set
(R) . [(b + n),a] is set
(R,a,b) is Element of the carrier of R
(R) . (b,a) is Element of the carrier of R
[b,a] is V15() set
(R) . [b,a] is set
(R,a,n) is Element of the carrier of R
(R) . (n,a) is Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
(R,a,b) + (R,a,n) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((R,a,b),(R,a,n)) is Element of the carrier of R
[(R,a,b),(R,a,n)] is V15() set
the addF of R . [(R,a,b),(R,a,n)] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(n + n)) is Element of the carrier of R
(R) . ((n + n),a) is Element of the carrier of R
[(n + n),a] is V15() set
(R) . [(n + n),a] is set
(R,a,n) is Element of the carrier of R
(R) . (n,a) is Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
(R,a,n) + (R,a,n) is Element of the carrier of R
the addF of R . ((R,a,n),(R,a,n)) is Element of the carrier of R
[(R,a,n),(R,a,n)] is V15() set
the addF of R . [(R,a,n),(R,a,n)] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(n + 1) + n is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,((n + 1) + n)) is Element of the carrier of R
(R) . (((n + 1) + n),a) is Element of the carrier of R
[((n + 1) + n),a] is V15() set
(R) . [((n + 1) + n),a] is set
(n + n) + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,((n + n) + 1)) is Element of the carrier of R
(R) . (((n + n) + 1),a) is Element of the carrier of R
[((n + n) + 1),a] is V15() set
(R) . [((n + n) + 1),a] is set
a + ((R,a,n) + (R,a,n)) is Element of the carrier of R
the addF of R . (a,((R,a,n) + (R,a,n))) is Element of the carrier of R
[a,((R,a,n) + (R,a,n))] is V15() set
the addF of R . [a,((R,a,n) + (R,a,n))] is set
a + (R,a,n) is Element of the carrier of R
the addF of R . (a,(R,a,n)) is Element of the carrier of R
[a,(R,a,n)] is V15() set
the addF of R . [a,(R,a,n)] is set
(a + (R,a,n)) + (R,a,n) is Element of the carrier of R
the addF of R . ((a + (R,a,n)),(R,a,n)) is Element of the carrier of R
[(a + (R,a,n)),(R,a,n)] is V15() set
the addF of R . [(a + (R,a,n)),(R,a,n)] is set
(R,a,(n + 1)) is Element of the carrier of R
(R) . ((n + 1),a) is Element of the carrier of R
[(n + 1),a] is V15() set
(R) . [(n + 1),a] is set
(R,a,(n + 1)) + (R,a,n) is Element of the carrier of R
the addF of R . ((R,a,(n + 1)),(R,a,n)) is Element of the carrier of R
[(R,a,(n + 1)),(R,a,n)] is V15() set
the addF of R . [(R,a,(n + 1)),(R,a,n)] is set
0 + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(0 + n)) is Element of the carrier of R
(R) . ((0 + n),a) is Element of the carrier of R
[(0 + n),a] is V15() set
(R) . [(0 + n),a] is set
0. R is V54(R) Element of the carrier of R
(0. R) + (R,a,n) is Element of the carrier of R
the addF of R . ((0. R),(R,a,n)) is Element of the carrier of R
[(0. R),(R,a,n)] is V15() set
the addF of R . [(0. R),(R,a,n)] is set
(R,a,0) is Element of the carrier of R
(R) . (0,a) is Element of the carrier of R
[0,a] is V15() set
(R) . [0,a] is set
(R,a,0) + (R,a,n) is Element of the carrier of R
the addF of R . ((R,a,0),(R,a,n)) is Element of the carrier of R
[(R,a,0),(R,a,n)] is V15() set
the addF of R . [(R,a,0),(R,a,n)] is set
R is non empty add-associative right_zeroed addLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
b + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(b + n)) is Element of the carrier of R
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(R) . (a,(b + n)) is Element of the carrier of R
[a,(b + n)] is V15() set
(R) . [a,(b + n)] is set
(R,a,b) is Element of the carrier of R
(R) . (a,b) is Element of the carrier of R
[a,b] is V15() set
(R) . [a,b] is set
(R,a,n) is Element of the carrier of R
(R) . (a,n) is Element of the carrier of R
[a,n] is V15() set
(R) . [a,n] is set
(R,a,b) + (R,a,n) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((R,a,b),(R,a,n)) is Element of the carrier of R
[(R,a,b),(R,a,n)] is V15() set
the addF of R . [(R,a,b),(R,a,n)] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
b + n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(b + n)) is Element of the carrier of R
(R) . (a,(b + n)) is Element of the carrier of R
[a,(b + n)] is V15() set
(R) . [a,(b + n)] is set
(R,a,n) is Element of the carrier of R
(R) . (a,n) is Element of the carrier of R
[a,n] is V15() set
(R) . [a,n] is set
(R,a,b) + (R,a,n) is Element of the carrier of R
the addF of R . ((R,a,b),(R,a,n)) is Element of the carrier of R
[(R,a,b),(R,a,n)] is V15() set
the addF of R . [(R,a,b),(R,a,n)] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
b + (n + 1) is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,(b + (n + 1))) is Element of the carrier of R
(R) . (a,(b + (n + 1))) is Element of the carrier of R
[a,(b + (n + 1))] is V15() set
(R) . [a,(b + (n + 1))] is set
(b + n) + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,((b + n) + 1)) is Element of the carrier of R
(R) . (a,((b + n) + 1)) is Element of the carrier of R
[a,((b + n) + 1)] is V15() set
(R) . [a,((b + n) + 1)] is set
((R,a,b) + (R,a,n)) + a is Element of the carrier of R
the addF of R . (((R,a,b) + (R,a,n)),a) is Element of the carrier of R
[((R,a,b) + (R,a,n)),a] is V15() set
the addF of R . [((R,a,b) + (R,a,n)),a] is set
(R,a,n) + a is Element of the carrier of R
the addF of R . ((R,a,n),a) is Element of the carrier of R
[(R,a,n),a] is V15() set
the addF of R . [(R,a,n),a] is set
(R,a,b) + ((R,a,n) + a) is Element of the carrier of R
the addF of R . ((R,a,b),((R,a,n) + a)) is Element of the carrier of R
[(R,a,b),((R,a,n) + a)] is V15() set
the addF of R . [(R,a,b),((R,a,n) + a)] is set
(R,a,(n + 1)) is Element of the carrier of R
(R) . (a,(n + 1)) is Element of the carrier of R
[a,(n + 1)] is V15() set
(R) . [a,(n + 1)] is set
(R,a,b) + (R,a,(n + 1)) is Element of the carrier of R
the addF of R . ((R,a,b),(R,a,(n + 1))) is Element of the carrier of R
[(R,a,b),(R,a,(n + 1))] is V15() set
the addF of R . [(R,a,b),(R,a,(n + 1))] is set
b + 0 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,(b + 0)) is Element of the carrier of R
(R) . (a,(b + 0)) is Element of the carrier of R
[a,(b + 0)] is V15() set
(R) . [a,(b + 0)] is set
0. R is V54(R) Element of the carrier of R
(R,a,b) + (0. R) is Element of the carrier of R
the addF of R . ((R,a,b),(0. R)) is Element of the carrier of R
[(R,a,b),(0. R)] is V15() set
the addF of R . [(R,a,b),(0. R)] is set
(R,a,0) is Element of the carrier of R
(R) . (a,0) is Element of the carrier of R
[a,0] is V15() set
(R) . [a,0] is set
(R,a,b) + (R,a,0) is Element of the carrier of R
the addF of R . ((R,a,b),(R,a,0)) is Element of the carrier of R
[(R,a,b),(R,a,0)] is V15() set
the addF of R . [(R,a,b),(R,a,0)] is set
R is non empty left_zeroed add-associative right_zeroed addLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,b) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . (b,a) is Element of the carrier of R
[b,a] is V15() set
(R) . [b,a] is set
(R,a,b) is Element of the carrier of R
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(R) . (a,b) is Element of the carrier of R
[a,b] is V15() set
(R) . [a,b] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,n) is Element of the carrier of R
(R) . (n,a) is Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
(R,a,n) is Element of the carrier of R
(R) . (a,n) is Element of the carrier of R
[a,n] is V15() set
(R) . [a,n] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,(n + 1)) is Element of the carrier of R
(R) . ((n + 1),a) is Element of the carrier of R
[(n + 1),a] is V15() set
(R) . [(n + 1),a] is set
(R,a,1) is Element of the carrier of R
(R) . (1,a) is Element of the carrier of R
[1,a] is V15() set
(R) . [1,a] is set
(R,a,n) + (R,a,1) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . ((R,a,n),(R,a,1)) is Element of the carrier of R
[(R,a,n),(R,a,1)] is V15() set
the addF of R . [(R,a,n),(R,a,1)] is set
(R,a,n) + a is Element of the carrier of R
the addF of R . ((R,a,n),a) is Element of the carrier of R
[(R,a,n),a] is V15() set
the addF of R . [(R,a,n),a] is set
(R,a,1) is Element of the carrier of R
(R) . (a,1) is Element of the carrier of R
[a,1] is V15() set
(R) . [a,1] is set
(R,a,n) + (R,a,1) is Element of the carrier of R
the addF of R . ((R,a,n),(R,a,1)) is Element of the carrier of R
[(R,a,n),(R,a,1)] is V15() set
the addF of R . [(R,a,n),(R,a,1)] is set
(R,a,(n + 1)) is Element of the carrier of R
(R) . (a,(n + 1)) is Element of the carrier of R
[a,(n + 1)] is V15() set
(R) . [a,(n + 1)] is set
(R,a,0) is Element of the carrier of R
(R) . (0,a) is Element of the carrier of R
[0,a] is V15() set
(R) . [0,a] is set
0. R is V54(R) Element of the carrier of R
(R,a,0) is Element of the carrier of R
(R) . (a,0) is Element of the carrier of R
[a,0] is V15() set
(R) . [a,0] is set
R is non empty Abelian addLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
b is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,b) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . (b,a) is Element of the carrier of R
[b,a] is V15() set
(R) . [b,a] is set
(R,a,b) is Element of the carrier of R
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(R) . (a,b) is Element of the carrier of R
[a,b] is V15() set
(R) . [a,b] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,n) is Element of the carrier of R
(R) . (n,a) is Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
(R,a,n) is Element of the carrier of R
(R) . (a,n) is Element of the carrier of R
[a,n] is V15() set
(R) . [a,n] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,(n + 1)) is Element of the carrier of R
(R) . ((n + 1),a) is Element of the carrier of R
[(n + 1),a] is V15() set
(R) . [(n + 1),a] is set
a + (R,a,n) is Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . (a,(R,a,n)) is Element of the carrier of R
[a,(R,a,n)] is V15() set
the addF of R . [a,(R,a,n)] is set
(R,a,(n + 1)) is Element of the carrier of R
(R) . (a,(n + 1)) is Element of the carrier of R
[a,(n + 1)] is V15() set
(R) . [a,(n + 1)] is set
(R,a,0) is Element of the carrier of R
(R) . (0,a) is Element of the carrier of R
[0,a] is V15() set
(R) . [0,a] is set
0. R is V54(R) Element of the carrier of R
(R,a,0) is Element of the carrier of R
(R) . (a,0) is Element of the carrier of R
[a,0] is V15() set
(R) . [a,0] is set
R is non empty left_add-cancelable left_zeroed left-distributive add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
a is left_add-cancelable Element of the carrier of R
b is left_add-cancelable Element of the carrier of R
a * b is left_add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . (a,b) is left_add-cancelable Element of the carrier of R
[a,b] is V15() set
the multF of R . [a,b] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,n) is left_add-cancelable Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . (n,a) is left_add-cancelable Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
(R,a,n) * b is left_add-cancelable Element of the carrier of R
the multF of R . ((R,a,n),b) is left_add-cancelable Element of the carrier of R
[(R,a,n),b] is V15() set
the multF of R . [(R,a,n),b] is set
(R,(a * b),n) is left_add-cancelable Element of the carrier of R
(R) . (n,(a * b)) is left_add-cancelable Element of the carrier of R
[n,(a * b)] is V15() set
(R) . [n,(a * b)] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,n) is left_add-cancelable Element of the carrier of R
(R) . (n,a) is left_add-cancelable Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
(R,a,n) * b is left_add-cancelable Element of the carrier of R
the multF of R . ((R,a,n),b) is left_add-cancelable Element of the carrier of R
[(R,a,n),b] is V15() set
the multF of R . [(R,a,n),b] is set
(R,(a * b),n) is left_add-cancelable Element of the carrier of R
(R) . (n,(a * b)) is left_add-cancelable Element of the carrier of R
[n,(a * b)] is V15() set
(R) . [n,(a * b)] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,(n + 1)) is left_add-cancelable Element of the carrier of R
(R) . ((n + 1),a) is left_add-cancelable Element of the carrier of R
[(n + 1),a] is V15() set
(R) . [(n + 1),a] is set
(R,a,(n + 1)) * b is left_add-cancelable Element of the carrier of R
the multF of R . ((R,a,(n + 1)),b) is left_add-cancelable Element of the carrier of R
[(R,a,(n + 1)),b] is V15() set
the multF of R . [(R,a,(n + 1)),b] is set
a + (R,a,n) is left_add-cancelable Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the addF of R . (a,(R,a,n)) is left_add-cancelable Element of the carrier of R
[a,(R,a,n)] is V15() set
the addF of R . [a,(R,a,n)] is set
(a + (R,a,n)) * b is left_add-cancelable Element of the carrier of R
the multF of R . ((a + (R,a,n)),b) is left_add-cancelable Element of the carrier of R
[(a + (R,a,n)),b] is V15() set
the multF of R . [(a + (R,a,n)),b] is set
(a * b) + (R,(a * b),n) is left_add-cancelable Element of the carrier of R
the addF of R . ((a * b),(R,(a * b),n)) is left_add-cancelable Element of the carrier of R
[(a * b),(R,(a * b),n)] is V15() set
the addF of R . [(a * b),(R,(a * b),n)] is set
(R,(a * b),1) is left_add-cancelable Element of the carrier of R
(R) . (1,(a * b)) is left_add-cancelable Element of the carrier of R
[1,(a * b)] is V15() set
(R) . [1,(a * b)] is set
(R,(a * b),1) + (R,(a * b),n) is left_add-cancelable Element of the carrier of R
the addF of R . ((R,(a * b),1),(R,(a * b),n)) is left_add-cancelable Element of the carrier of R
[(R,(a * b),1),(R,(a * b),n)] is V15() set
the addF of R . [(R,(a * b),1),(R,(a * b),n)] is set
(R,(a * b),(n + 1)) is left_add-cancelable Element of the carrier of R
(R) . ((n + 1),(a * b)) is left_add-cancelable Element of the carrier of R
[(n + 1),(a * b)] is V15() set
(R) . [(n + 1),(a * b)] is set
(R,a,0) is left_add-cancelable Element of the carrier of R
(R) . (0,a) is left_add-cancelable Element of the carrier of R
[0,a] is V15() set
(R) . [0,a] is set
(R,a,0) * b is left_add-cancelable Element of the carrier of R
the multF of R . ((R,a,0),b) is left_add-cancelable Element of the carrier of R
[(R,a,0),b] is V15() set
the multF of R . [(R,a,0),b] is set
0. R is V54(R) left_add-cancelable Element of the carrier of R
(0. R) * b is left_add-cancelable Element of the carrier of R
the multF of R . ((0. R),b) is left_add-cancelable Element of the carrier of R
[(0. R),b] is V15() set
the multF of R . [(0. R),b] is set
(R,(a * b),0) is left_add-cancelable Element of the carrier of R
(R) . (0,(a * b)) is left_add-cancelable Element of the carrier of R
[0,(a * b)] is V15() set
(R) . [0,(a * b)] is set
R is non empty right_add-cancelable left_zeroed right-distributive left-distributive distributive add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
b is right_add-cancelable Element of the carrier of R
a is right_add-cancelable Element of the carrier of R
b * a is right_add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . (b,a) is right_add-cancelable Element of the carrier of R
[b,a] is V15() set
the multF of R . [b,a] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,n) is right_add-cancelable Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . (n,a) is right_add-cancelable Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
b * (R,a,n) is right_add-cancelable Element of the carrier of R
the multF of R . (b,(R,a,n)) is right_add-cancelable Element of the carrier of R
[b,(R,a,n)] is V15() set
the multF of R . [b,(R,a,n)] is set
(R,(b * a),n) is right_add-cancelable Element of the carrier of R
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(R) . ((b * a),n) is right_add-cancelable Element of the carrier of R
[(b * a),n] is V15() set
(R) . [(b * a),n] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,n) is right_add-cancelable Element of the carrier of R
(R) . (n,a) is right_add-cancelable Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
b * (R,a,n) is right_add-cancelable Element of the carrier of R
the multF of R . (b,(R,a,n)) is right_add-cancelable Element of the carrier of R
[b,(R,a,n)] is V15() set
the multF of R . [b,(R,a,n)] is set
(R,(b * a),n) is right_add-cancelable Element of the carrier of R
(R) . ((b * a),n) is right_add-cancelable Element of the carrier of R
[(b * a),n] is V15() set
(R) . [(b * a),n] is set
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,(n + 1)) is right_add-cancelable Element of the carrier of R
(R) . ((n + 1),a) is right_add-cancelable Element of the carrier of R
[(n + 1),a] is V15() set
(R) . [(n + 1),a] is set
b * (R,a,(n + 1)) is right_add-cancelable Element of the carrier of R
the multF of R . (b,(R,a,(n + 1))) is right_add-cancelable Element of the carrier of R
[b,(R,a,(n + 1))] is V15() set
the multF of R . [b,(R,a,(n + 1))] is set
a + (R,a,n) is right_add-cancelable Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the addF of R . (a,(R,a,n)) is right_add-cancelable Element of the carrier of R
[a,(R,a,n)] is V15() set
the addF of R . [a,(R,a,n)] is set
b * (a + (R,a,n)) is right_add-cancelable Element of the carrier of R
the multF of R . (b,(a + (R,a,n))) is right_add-cancelable Element of the carrier of R
[b,(a + (R,a,n))] is V15() set
the multF of R . [b,(a + (R,a,n))] is set
(b * a) + (R,(b * a),n) is right_add-cancelable Element of the carrier of R
the addF of R . ((b * a),(R,(b * a),n)) is right_add-cancelable Element of the carrier of R
[(b * a),(R,(b * a),n)] is V15() set
the addF of R . [(b * a),(R,(b * a),n)] is set
(R,(b * a),1) is right_add-cancelable Element of the carrier of R
(R) . ((b * a),1) is right_add-cancelable Element of the carrier of R
[(b * a),1] is V15() set
(R) . [(b * a),1] is set
(R,(b * a),1) + (R,(b * a),n) is right_add-cancelable Element of the carrier of R
the addF of R . ((R,(b * a),1),(R,(b * a),n)) is right_add-cancelable Element of the carrier of R
[(R,(b * a),1),(R,(b * a),n)] is V15() set
the addF of R . [(R,(b * a),1),(R,(b * a),n)] is set
(R,(b * a),(n + 1)) is right_add-cancelable Element of the carrier of R
(R) . ((b * a),(n + 1)) is right_add-cancelable Element of the carrier of R
[(b * a),(n + 1)] is V15() set
(R) . [(b * a),(n + 1)] is set
(R,a,0) is right_add-cancelable Element of the carrier of R
(R) . (0,a) is right_add-cancelable Element of the carrier of R
[0,a] is V15() set
(R) . [0,a] is set
b * (R,a,0) is right_add-cancelable Element of the carrier of R
the multF of R . (b,(R,a,0)) is right_add-cancelable Element of the carrier of R
[b,(R,a,0)] is V15() set
the multF of R . [b,(R,a,0)] is set
0. R is V54(R) right_add-cancelable Element of the carrier of R
b * (0. R) is right_add-cancelable Element of the carrier of R
the multF of R . (b,(0. R)) is right_add-cancelable Element of the carrier of R
[b,(0. R)] is V15() set
the multF of R . [b,(0. R)] is set
(R,(b * a),0) is right_add-cancelable Element of the carrier of R
(R) . ((b * a),0) is right_add-cancelable Element of the carrier of R
[(b * a),0] is V15() set
(R) . [(b * a),0] is set
R is non empty left_add-cancelable right_add-cancelable add-cancelable left_zeroed right-distributive left-distributive distributive add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(R) . (a,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[a,n] is V15() set
(R) . [a,n] is set
(R,a,n) * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,a,n),b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,n),b] is V15() set
the multF of R . [(R,a,n),b] is set
(R,b,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . (n,b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[n,b] is V15() set
(R) . [n,b] is set
a * (R,b,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (a,(R,b,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[a,(R,b,n)] is V15() set
the multF of R . [a,(R,b,n)] is set
(R,a,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . (n,a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[n,a] is V15() set
(R) . [n,a] is set
(R,a,n) * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,a,n),b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,n),b] is V15() set
the multF of R . [(R,a,n),b] is set
a * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (a,b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[a,b] is V15() set
the multF of R . [a,b] is set
(R,(a * b),n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . (n,(a * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[n,(a * b)] is V15() set
(R) . [n,(a * b)] is set
(R,(a * b),n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . ((a * b),n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(a * b),n] is V15() set
(R) . [(a * b),n] is set
R is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
a is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
a choose R is set
R is non empty unital doubleLoopStr
the carrier of R is non empty set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
a is Element of the carrier of R
b is Element of the carrier of R
Seg (n + 1) is non empty V35() V42(n + 1) Element of bool NAT
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - 1 is V31() V32() V33() ext-real set
(n + 1) - 1 is V31() V32() V33() ext-real set
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - G1 is V31() V32() V33() ext-real set
G2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,G2) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,G2) is set
[a,G2] is V15() set
(power R) . [a,G2] is set
(G1,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,G2),(G1,n)) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . ((G1,n),(R,a,G2)) is Element of the carrier of R
[(G1,n),(R,a,G2)] is V15() set
(R) . [(G1,n),(R,a,G2)] is set
(R,b,G1) is Element of the carrier of R
(power R) . (b,G1) is set
[b,G1] is V15() set
(power R) . [b,G1] is set
(R,(R,a,G2),(G1,n)) * (R,b,G1) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,(R,a,G2),(G1,n)),(R,b,G1)) is Element of the carrier of R
[(R,(R,a,G2),(G1,n)),(R,b,G1)] is V15() set
the multF of R . [(R,(R,a,G2),(G1,n)),(R,b,G1)] is set
F1 is Element of the carrier of R
F is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
F2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - F is V31() V32() V33() ext-real set
(R,a,F2) is Element of the carrier of R
(power R) . (a,F2) is set
[a,F2] is V15() set
(power R) . [a,F2] is set
(F,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,F2),(F,n)) is Element of the carrier of R
(R) . ((F,n),(R,a,F2)) is Element of the carrier of R
[(F,n),(R,a,F2)] is V15() set
(R) . [(F,n),(R,a,F2)] is set
(R,b,F) is Element of the carrier of R
(power R) . (b,F) is set
[b,F] is V15() set
(power R) . [b,F] is set
(R,(R,a,F2),(F,n)) * (R,b,F) is Element of the carrier of R
the multF of R . ((R,(R,a,F2),(F,n)),(R,b,F)) is Element of the carrier of R
[(R,(R,a,F2),(F,n)),(R,b,F)] is V15() set
the multF of R . [(R,(R,a,F2),(F,n)),(R,b,F)] is set
n is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
dom n is Element of bool NAT
len n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
F1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
G1 - 1 is V31() V32() V33() ext-real set
G2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - F1 is V31() V32() V33() ext-real set
n /. G1 is Element of the carrier of R
(R,a,G2) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,G2) is set
[a,G2] is V15() set
(power R) . [a,G2] is set
(F1,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,G2),(F1,n)) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . ((F1,n),(R,a,G2)) is Element of the carrier of R
[(F1,n),(R,a,G2)] is V15() set
(R) . [(F1,n),(R,a,G2)] is set
(R,b,F1) is Element of the carrier of R
(power R) . (b,F1) is set
[b,F1] is V15() set
(power R) . [b,F1] is set
(R,(R,a,G2),(F1,n)) * (R,b,F1) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,(R,a,G2),(F1,n)),(R,b,F1)) is Element of the carrier of R
[(R,(R,a,G2),(F1,n)),(R,b,F1)] is V15() set
the multF of R . [(R,(R,a,G2),(F1,n)),(R,b,F1)] is set
n is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
dom n is Element of bool NAT
G1 is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
dom G1 is Element of bool NAT
G2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
n . G2 is set
G1 . G2 is set
G2 - 1 is V31() V32() V33() ext-real set
(n + 1) - 1 is V31() V32() V33() ext-real set
F1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - F1 is V31() V32() V33() ext-real set
Seg (n + 1) is non empty V35() V42(n + 1) Element of bool NAT
G1 /. G2 is Element of the carrier of R
F2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,F2) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,F2) is set
[a,F2] is V15() set
(power R) . [a,F2] is set
(F1,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,F2),(F1,n)) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . ((F1,n),(R,a,F2)) is Element of the carrier of R
[(F1,n),(R,a,F2)] is V15() set
(R) . [(F1,n),(R,a,F2)] is set
(R,b,F1) is Element of the carrier of R
(power R) . (b,F1) is set
[b,F1] is V15() set
(power R) . [b,F1] is set
(R,(R,a,F2),(F1,n)) * (R,b,F1) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,(R,a,F2),(F1,n)),(R,b,F1)) is Element of the carrier of R
[(R,(R,a,F2),(F1,n)),(R,b,F1)] is V15() set
the multF of R . [(R,(R,a,F2),(F1,n)),(R,b,F1)] is set
n /. G2 is Element of the carrier of R
R is non empty unital right_zeroed doubleLoopStr
the carrier of R is non empty set
1_ R is Element of the carrier of R
<*(1_ R)*> is V1() V4( NAT ) V5( the carrier of R) Function-like non empty trivial V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of R
a is Element of the carrier of R
b is Element of the carrier of R
(R,a,b,0) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len (R,a,b,0) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
dom (R,a,b,0) is Element of bool NAT
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - 1 is V31() V32() V33() ext-real set
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
0 - G1 is V31() V32() V33() ext-real non positive set
(R,a,b,0) . 1 is set
(R,a,b,0) /. 1 is Element of the carrier of R
G2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,G2) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (a,G2) is set
[a,G2] is V15() set
(power R) . [a,G2] is set
(G1,0) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,G2),(G1,0)) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . ((G1,0),(R,a,G2)) is Element of the carrier of R
[(G1,0),(R,a,G2)] is V15() set
(R) . [(G1,0),(R,a,G2)] is set
(R,b,G1) is Element of the carrier of R
(power R) . (b,G1) is set
[b,G1] is V15() set
(power R) . [b,G1] is set
(R,(R,a,G2),(G1,0)) * (R,b,G1) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,(R,a,G2),(G1,0)),(R,b,G1)) is Element of the carrier of R
[(R,(R,a,G2),(G1,0)),(R,b,G1)] is V15() set
the multF of R . [(R,(R,a,G2),(G1,0)),(R,b,G1)] is set
(R,(R,a,G2),1) is Element of the carrier of R
(R) . (1,(R,a,G2)) is Element of the carrier of R
[1,(R,a,G2)] is V15() set
(R) . [1,(R,a,G2)] is set
(R,(R,a,G2),1) * (R,b,G1) is Element of the carrier of R
the multF of R . ((R,(R,a,G2),1),(R,b,G1)) is Element of the carrier of R
[(R,(R,a,G2),1),(R,b,G1)] is V15() set
the multF of R . [(R,(R,a,G2),1),(R,b,G1)] is set
(R,a,0) is Element of the carrier of R
(power R) . (a,0) is set
[a,0] is V15() set
(power R) . [a,0] is set
(R,(R,a,0),1) is Element of the carrier of R
(R) . (1,(R,a,0)) is Element of the carrier of R
[1,(R,a,0)] is V15() set
(R) . [1,(R,a,0)] is set
(R,(R,a,0),1) * (1_ R) is Element of the carrier of R
the multF of R . ((R,(R,a,0),1),(1_ R)) is Element of the carrier of R
[(R,(R,a,0),1),(1_ R)] is V15() set
the multF of R . [(R,(R,a,0),1),(1_ R)] is set
(R,(1_ R),1) is Element of the carrier of R
(R) . (1,(1_ R)) is Element of the carrier of R
[1,(1_ R)] is V15() set
(R) . [1,(1_ R)] is set
(R,(1_ R),1) * (1_ R) is Element of the carrier of R
the multF of R . ((R,(1_ R),1),(1_ R)) is Element of the carrier of R
[(R,(1_ R),1),(1_ R)] is V15() set
the multF of R . [(R,(1_ R),1),(1_ R)] is set
(1_ R) * (1_ R) is Element of the carrier of R
the multF of R . ((1_ R),(1_ R)) is Element of the carrier of R
[(1_ R),(1_ R)] is V15() set
the multF of R . [(1_ R),(1_ R)] is set
1 - 1 is V31() V32() V33() ext-real set
a is non empty unital right_zeroed doubleLoopStr
the carrier of a is non empty set
b is Element of the carrier of a
n is Element of the carrier of a
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(a,b,n,n) is V1() V4( NAT ) V5( the carrier of a) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of a
(a,b,n,n) . 1 is set
(a,b,n) is Element of the carrier of a
power a is V1() V4([: the carrier of a,NAT:]) V5( the carrier of a) Function-like quasi_total Element of bool [:[: the carrier of a,NAT:], the carrier of a:]
[: the carrier of a,NAT:] is V35() set
[:[: the carrier of a,NAT:], the carrier of a:] is V35() set
bool [:[: the carrier of a,NAT:], the carrier of a:] is V35() set
(power a) . (b,n) is set
[b,n] is V15() set
(power a) . [b,n] is set
R is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - R is V31() V32() V33() ext-real set
len (a,b,n,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
dom (a,b,n,n) is Element of bool NAT
Seg (n + 1) is non empty V35() V42(n + 1) Element of bool NAT
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(a,b,n,n) /. 1 is Element of the carrier of a
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(a,b,G1) is Element of the carrier of a
(power a) . (b,G1) is set
[b,G1] is V15() set
(power a) . [b,G1] is set
(0,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(a,(a,b,G1),(0,n)) is Element of the carrier of a
(a) is V1() V4([:NAT, the carrier of a:]) V5( the carrier of a) Function-like quasi_total Element of bool [:[:NAT, the carrier of a:], the carrier of a:]
[:NAT, the carrier of a:] is V35() set
[:[:NAT, the carrier of a:], the carrier of a:] is V35() set
bool [:[:NAT, the carrier of a:], the carrier of a:] is V35() set
(a) . ((0,n),(a,b,G1)) is Element of the carrier of a
[(0,n),(a,b,G1)] is V15() set
(a) . [(0,n),(a,b,G1)] is set
(a,n,R) is Element of the carrier of a
(power a) . (n,R) is set
[n,R] is V15() set
(power a) . [n,R] is set
(a,(a,b,G1),(0,n)) * (a,n,R) is Element of the carrier of a
the multF of a is V1() V4([: the carrier of a, the carrier of a:]) V5( the carrier of a) Function-like quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]
[: the carrier of a, the carrier of a:] is set
[:[: the carrier of a, the carrier of a:], the carrier of a:] is set
bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is set
the multF of a . ((a,(a,b,G1),(0,n)),(a,n,R)) is Element of the carrier of a
[(a,(a,b,G1),(0,n)),(a,n,R)] is V15() set
the multF of a . [(a,(a,b,G1),(0,n)),(a,n,R)] is set
(a,(a,b,n),1) is Element of the carrier of a
(a) . (1,(a,b,n)) is Element of the carrier of a
[1,(a,b,n)] is V15() set
(a) . [1,(a,b,n)] is set
(a,n,0) is Element of the carrier of a
(power a) . (n,0) is set
[n,0] is V15() set
(power a) . [n,0] is set
(a,(a,b,n),1) * (a,n,0) is Element of the carrier of a
the multF of a . ((a,(a,b,n),1),(a,n,0)) is Element of the carrier of a
[(a,(a,b,n),1),(a,n,0)] is V15() set
the multF of a . [(a,(a,b,n),1),(a,n,0)] is set
(a,b,n) * (a,n,0) is Element of the carrier of a
the multF of a . ((a,b,n),(a,n,0)) is Element of the carrier of a
[(a,b,n),(a,n,0)] is V15() set
the multF of a . [(a,b,n),(a,n,0)] is set
1_ a is Element of the carrier of a
(a,b,n) * (1_ a) is Element of the carrier of a
the multF of a . ((a,b,n),(1_ a)) is Element of the carrier of a
[(a,b,n),(1_ a)] is V15() set
the multF of a . [(a,b,n),(1_ a)] is set
R is non empty unital right_zeroed doubleLoopStr
the carrier of R is non empty set
a is Element of the carrier of R
b is Element of the carrier of R
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,b,n) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,a,b,n) . (n + 1) is set
(R,b,n) is Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . (b,n) is set
[b,n] is V15() set
(power R) . [b,n] is set
(n + 1) - 1 is V31() V32() V33() ext-real set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - n is V31() V32() V33() ext-real set
len (R,a,b,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
dom (R,a,b,n) is Element of bool NAT
Seg (n + 1) is non empty V35() V42(n + 1) Element of bool NAT
G1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,b,n) /. (n + 1) is Element of the carrier of R
(R,a,0) is Element of the carrier of R
(power R) . (a,0) is set
[a,0] is V15() set
(power R) . [a,0] is set
(n,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,0),(n,n)) is Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . ((n,n),(R,a,0)) is Element of the carrier of R
[(n,n),(R,a,0)] is V15() set
(R) . [(n,n),(R,a,0)] is set
(R,(R,a,0),(n,n)) * (R,b,n) is Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the multF of R . ((R,(R,a,0),(n,n)),(R,b,n)) is Element of the carrier of R
[(R,(R,a,0),(n,n)),(R,b,n)] is V15() set
the multF of R . [(R,(R,a,0),(n,n)),(R,b,n)] is set
(R,(R,a,0),1) is Element of the carrier of R
(R) . (1,(R,a,0)) is Element of the carrier of R
[1,(R,a,0)] is V15() set
(R) . [1,(R,a,0)] is set
(R,(R,a,0),1) * (R,b,n) is Element of the carrier of R
the multF of R . ((R,(R,a,0),1),(R,b,n)) is Element of the carrier of R
[(R,(R,a,0),1),(R,b,n)] is V15() set
the multF of R . [(R,(R,a,0),1),(R,b,n)] is set
1_ R is Element of the carrier of R
(R,(1_ R),1) is Element of the carrier of R
(R) . (1,(1_ R)) is Element of the carrier of R
[1,(1_ R)] is V15() set
(R) . [1,(1_ R)] is set
(R,(1_ R),1) * (R,b,n) is Element of the carrier of R
the multF of R . ((R,(1_ R),1),(R,b,n)) is Element of the carrier of R
[(R,(1_ R),1),(R,b,n)] is V15() set
the multF of R . [(R,(1_ R),1),(R,b,n)] is set
(1_ R) * (R,b,n) is Element of the carrier of R
the multF of R . ((1_ R),(R,b,n)) is Element of the carrier of R
[(1_ R),(R,b,n)] is V15() set
the multF of R . [(1_ R),(R,b,n)] is set
R is non empty left_add-cancelable right_add-cancelable add-cancelable left_zeroed unital associative commutative right-distributive left-distributive distributive Abelian add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
a + b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is set
the addF of R . (a,b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[a,b] is V15() set
the addF of R . [a,b] is set
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(a + b),n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
power R is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
[: the carrier of R,NAT:] is V35() set
[:[: the carrier of R,NAT:], the carrier of R:] is V35() set
bool [:[: the carrier of R,NAT:], the carrier of R:] is V35() set
(power R) . ((a + b),n) is set
[(a + b),n] is V15() set
(power R) . [(a + b),n] is set
(R,a,b,n) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,a,b,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
n is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(a + b),n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . ((a + b),n) is set
[(a + b),n] is V15() set
(power R) . [(a + b),n] is set
(R,a,b,n) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,a,b,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
n + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(R,(a + b),(n + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . ((a + b),(n + 1)) is set
[(a + b),(n + 1)] is V15() set
(power R) . [(a + b),(n + 1)] is set
(R,a,b,(n + 1)) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,a,b,(n + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R,a,b,n) * a is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
0. R is V54(R) left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
<*(0. R)*> is V1() V4( NAT ) V5( the carrier of R) Function-like non empty trivial V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of R
((R,a,b,n) * a) ^ <*(0. R)*> is V1() V4( NAT ) V5( the carrier of R) Function-like non empty V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
(R,a,b,n) * b is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
<*(0. R)*> ^ ((R,a,b,n) * b) is V1() V4( NAT ) V5( the carrier of R) Function-like non empty V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len ((R,a,b,n) * a) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
Seg (len ((R,a,b,n) * a)) is V35() V42( len ((R,a,b,n) * a)) Element of bool NAT
dom ((R,a,b,n) * a) is Element of bool NAT
dom (R,a,b,n) is Element of bool NAT
len (R,a,b,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
Seg (len (R,a,b,n)) is V35() V42( len (R,a,b,n)) Element of bool NAT
len (((R,a,b,n) * a) ^ <*(0. R)*>) is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
len <*(0. R)*> is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(len ((R,a,b,n) * a)) + (len <*(0. R)*>) is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(len ((R,a,b,n) * a)) + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(len (R,a,b,n)) + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(n + 1) + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
((n + 1) + 1) -tuples_on the carrier of R is functional non empty FinSequence-membered FinSequenceSet of the carrier of R
len ((R,a,b,n) * b) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
Seg (len ((R,a,b,n) * b)) is V35() V42( len ((R,a,b,n) * b)) Element of bool NAT
dom ((R,a,b,n) * b) is Element of bool NAT
len (<*(0. R)*> ^ ((R,a,b,n) * b)) is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(len ((R,a,b,n) * b)) + (len <*(0. R)*>) is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(len ((R,a,b,n) * b)) + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
F1 is V1() V4( NAT ) V5( the carrier of R) Function-like V35() V42((n + 1) + 1) FinSequence-like FinSubsequence-like Element of ((n + 1) + 1) -tuples_on the carrier of R
len F1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
F2 is V1() V4( NAT ) V5( the carrier of R) Function-like V35() V42((n + 1) + 1) FinSequence-like FinSubsequence-like Element of ((n + 1) + 1) -tuples_on the carrier of R
(R,F1,F2) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
len F2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
len (R,F1,F2) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
Seg (len (R,F1,F2)) is V35() V42( len (R,F1,F2)) Element of bool NAT
dom (R,F1,F2) is Element of bool NAT
dom F1 is V42((n + 1) + 1) Element of bool NAT
Seg (len F1) is V35() V42( len F1) Element of bool NAT
len (R,a,b,(n + 1)) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
i is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative set
(R,F1,F2) . i is set
(R,a,b,(n + 1)) . i is set
dom (R,a,b,(n + 1)) is Element of bool NAT
Seg ((n + 1) + 1) is non empty V35() V42((n + 1) + 1) Element of bool NAT
i - 1 is V31() V32() V33() ext-real set
j is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,b,n) /. j is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
F1 /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
F2 /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R,a,b,n) /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
j + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
dom F2 is V42((n + 1) + 1) Element of bool NAT
{((n + 1) + 1)} is non empty trivial V42(1) set
(((R,a,b,n) * a) ^ <*(0. R)*>) . ((len ((R,a,b,n) * a)) + 1) is set
((n + 1) + 1) - 1 is V31() V32() V33() ext-real set
Seg (n + 1) is non empty V35() V42(n + 1) Element of bool NAT
(R,a,b,n) . (n + 1) is set
(R,b,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (b,n) is set
[b,n] is V15() set
(power R) . [b,n] is set
1 + (n + 1) is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(<*(0. R)*> ^ ((R,a,b,n) * b)) . (1 + (n + 1)) is set
(len <*(0. R)*>) + j is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(<*(0. R)*> ^ ((R,a,b,n) * b)) . ((len <*(0. R)*>) + j) is set
((R,a,b,n) * b) . j is set
((R,a,b,n) * b) /. j is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R,b,n) * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . ((R,b,n),b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,b,n),b] is V15() set
the multF of R . [(R,b,n),b] is set
(R,b,(n + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (b,(n + 1)) is set
[b,(n + 1)] is V15() set
(power R) . [b,(n + 1)] is set
(R,F1,F2) /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(0. R) + (F2 /. i) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((0. R),(F2 /. i)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(0. R),(F2 /. i)] is V15() set
the addF of R . [(0. R),(F2 /. i)] is set
{ b₁ where b₁ is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not (n + 1) + 1 <= b₁ ) } is set
m2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
m2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
Seg (n + 1) is non empty V35() V42(n + 1) Element of bool NAT
m2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
m2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
j - 1 is V31() V32() V33() ext-real set
l2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(n + 1) - 1 is V31() V32() V33() ext-real set
m2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - m2 is V31() V32() V33() ext-real set
l1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(<*(0. R)*> ^ ((R,a,b,n) * b)) . i is set
(len <*(0. R)*>) + j is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(<*(0. R)*> ^ ((R,a,b,n) * b)) . ((len <*(0. R)*>) + j) is set
((R,a,b,n) * b) . j is set
((R,a,b,n) * b) /. j is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
((R,a,b,n) /. j) * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . (((R,a,b,n) /. j),b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,a,b,n) /. j),b] is V15() set
the multF of R . [((R,a,b,n) /. j),b] is set
m1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
n - m1 is V31() V32() V33() ext-real set
l1 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
l1 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
m2 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
(n + 1) - (m2 + 1) is V31() V32() V33() ext-real set
(((R,a,b,n) * a) ^ <*(0. R)*>) . i is set
((R,a,b,n) * a) . i is set
((R,a,b,n) * a) /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
((R,a,b,n) /. i) * a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (((R,a,b,n) /. i),a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,a,b,n) /. i),a] is V15() set
the multF of R . [((R,a,b,n) /. i),a] is set
(R,F1,F2) /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(F1 /. i) + (((R,a,b,n) /. j) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((F1 /. i),(((R,a,b,n) /. j) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(F1 /. i),(((R,a,b,n) /. j) * b)] is V15() set
the addF of R . [(F1 /. i),(((R,a,b,n) /. j) * b)] is set
(R,a,l1) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (a,l1) is set
[a,l1] is V15() set
(power R) . [a,l1] is set
(m1,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,l1),(m1,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) is V1() V4([:NAT, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[:NAT, the carrier of R:], the carrier of R:]
[:NAT, the carrier of R:] is V35() set
[:[:NAT, the carrier of R:], the carrier of R:] is V35() set
bool [:[:NAT, the carrier of R:], the carrier of R:] is V35() set
(R) . ((m1,n),(R,a,l1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(m1,n),(R,a,l1)] is V15() set
(R) . [(m1,n),(R,a,l1)] is set
(R,b,m1) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (b,m1) is set
[b,m1] is V15() set
(power R) . [b,m1] is set
(R,(R,a,l1),(m1,n)) * (R,b,m1) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,(R,a,l1),(m1,n)),(R,b,m1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,(R,a,l1),(m1,n)),(R,b,m1)] is V15() set
the multF of R . [(R,(R,a,l1),(m1,n)),(R,b,m1)] is set
((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (((R,(R,a,l1),(m1,n)) * (R,b,m1)),a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,(R,a,l1),(m1,n)) * (R,b,m1)),a] is V15() set
the multF of R . [((R,(R,a,l1),(m1,n)) * (R,b,m1)),a] is set
(((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a) + (((R,a,b,n) /. j) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a),(((R,a,b,n) /. j) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a),(((R,a,b,n) /. j) * b)] is V15() set
the addF of R . [(((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a),(((R,a,b,n) /. j) * b)] is set
(R,(R,a,l1),(m1,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) is V1() V4([: the carrier of R,NAT:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R,NAT:], the carrier of R:]
(R) . ((R,a,l1),(m1,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,l1),(m1,n)] is V15() set
(R) . [(R,a,l1),(m1,n)] is set
(R,(R,a,l1),(m1,n)) * (R,b,m1) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,(R,a,l1),(m1,n)),(R,b,m1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,(R,a,l1),(m1,n)),(R,b,m1)] is V15() set
the multF of R . [(R,(R,a,l1),(m1,n)),(R,b,m1)] is set
((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (((R,(R,a,l1),(m1,n)) * (R,b,m1)),a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,(R,a,l1),(m1,n)) * (R,b,m1)),a] is V15() set
the multF of R . [((R,(R,a,l1),(m1,n)) * (R,b,m1)),a] is set
(((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a) + (((R,a,b,n) /. j) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a),(((R,a,b,n) /. j) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a),(((R,a,b,n) /. j) * b)] is V15() set
the addF of R . [(((R,(R,a,l1),(m1,n)) * (R,b,m1)) * a),(((R,a,b,n) /. j) * b)] is set
(R,(R,b,m1),(m1,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . ((m1,n),(R,b,m1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(m1,n),(R,b,m1)] is V15() set
(R) . [(m1,n),(R,b,m1)] is set
(R,a,l1) * (R,(R,b,m1),(m1,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,a,l1),(R,(R,b,m1),(m1,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,l1),(R,(R,b,m1),(m1,n))] is V15() set
the multF of R . [(R,a,l1),(R,(R,b,m1),(m1,n))] is set
a * ((R,a,l1) * (R,(R,b,m1),(m1,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (a,((R,a,l1) * (R,(R,b,m1),(m1,n)))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[a,((R,a,l1) * (R,(R,b,m1),(m1,n)))] is V15() set
the multF of R . [a,((R,a,l1) * (R,(R,b,m1),(m1,n)))] is set
(a * ((R,a,l1) * (R,(R,b,m1),(m1,n)))) + (((R,a,b,n) /. j) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((a * ((R,a,l1) * (R,(R,b,m1),(m1,n)))),(((R,a,b,n) /. j) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(a * ((R,a,l1) * (R,(R,b,m1),(m1,n)))),(((R,a,b,n) /. j) * b)] is V15() set
the addF of R . [(a * ((R,a,l1) * (R,(R,b,m1),(m1,n)))),(((R,a,b,n) /. j) * b)] is set
a * (R,a,l1) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (a,(R,a,l1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[a,(R,a,l1)] is V15() set
the multF of R . [a,(R,a,l1)] is set
(a * (R,a,l1)) * (R,(R,b,m1),(m1,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((a * (R,a,l1)),(R,(R,b,m1),(m1,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(a * (R,a,l1)),(R,(R,b,m1),(m1,n))] is V15() set
the multF of R . [(a * (R,a,l1)),(R,(R,b,m1),(m1,n))] is set
((a * (R,a,l1)) * (R,(R,b,m1),(m1,n))) + (((R,a,b,n) /. j) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((a * (R,a,l1)) * (R,(R,b,m1),(m1,n))),(((R,a,b,n) /. j) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((a * (R,a,l1)) * (R,(R,b,m1),(m1,n))),(((R,a,b,n) /. j) * b)] is V15() set
the addF of R . [((a * (R,a,l1)) * (R,(R,b,m1),(m1,n))),(((R,a,b,n) /. j) * b)] is set
(R,a,(l1 + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (a,(l1 + 1)) is set
[a,(l1 + 1)] is V15() set
(power R) . [a,(l1 + 1)] is set
(R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,a,(l1 + 1)),(R,(R,b,m1),(m1,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,(l1 + 1)),(R,(R,b,m1),(m1,n))] is V15() set
the multF of R . [(R,a,(l1 + 1)),(R,(R,b,m1),(m1,n))] is set
((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))) + (((R,a,b,n) /. j) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,a,b,n) /. j) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,a,b,n) /. j) * b)] is V15() set
the addF of R . [((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,a,b,n) /. j) * b)] is set
(R,b,m2) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (b,m2) is set
[b,m2] is V15() set
(power R) . [b,m2] is set
l2 is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,a,l2) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (a,l2) is set
[a,l2] is V15() set
(power R) . [a,l2] is set
(m2,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,l2),(m2,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . ((m2,n),(R,a,l2)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(m2,n),(R,a,l2)] is V15() set
(R) . [(m2,n),(R,a,l2)] is set
(R,b,m2) * (R,(R,a,l2),(m2,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,b,m2),(R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,b,m2),(R,(R,a,l2),(m2,n))] is V15() set
the multF of R . [(R,b,m2),(R,(R,a,l2),(m2,n))] is set
((R,b,m2) * (R,(R,a,l2),(m2,n))) * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (((R,b,m2) * (R,(R,a,l2),(m2,n))),b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,b,m2) * (R,(R,a,l2),(m2,n))),b] is V15() set
the multF of R . [((R,b,m2) * (R,(R,a,l2),(m2,n))),b] is set
((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))) + (((R,b,m2) * (R,(R,a,l2),(m2,n))) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,b,m2) * (R,(R,a,l2),(m2,n))) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,b,m2) * (R,(R,a,l2),(m2,n))) * b)] is V15() set
the addF of R . [((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,b,m2) * (R,(R,a,l2),(m2,n))) * b)] is set
(R,b,m2) * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,b,m2),b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,b,m2),b] is V15() set
the multF of R . [(R,b,m2),b] is set
((R,b,m2) * b) * (R,(R,a,l2),(m2,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (((R,b,m2) * b),(R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,b,m2) * b),(R,(R,a,l2),(m2,n))] is V15() set
the multF of R . [((R,b,m2) * b),(R,(R,a,l2),(m2,n))] is set
((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))) + (((R,b,m2) * b) * (R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,b,m2) * b) * (R,(R,a,l2),(m2,n)))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,b,m2) * b) * (R,(R,a,l2),(m2,n)))] is V15() set
the addF of R . [((R,a,(l1 + 1)) * (R,(R,b,m1),(m1,n))),(((R,b,m2) * b) * (R,(R,a,l2),(m2,n)))] is set
(R,b,(m2 + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (b,(m2 + 1)) is set
[b,(m2 + 1)] is V15() set
(power R) . [b,(m2 + 1)] is set
((m2 + 1),n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,b,(m2 + 1)),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . (((m2 + 1),n),(R,b,(m2 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((m2 + 1),n),(R,b,(m2 + 1))] is V15() set
(R) . [((m2 + 1),n),(R,b,(m2 + 1))] is set
(R,a,(l1 + 1)) * (R,(R,b,(m2 + 1)),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,a,(l1 + 1)),(R,(R,b,(m2 + 1)),((m2 + 1),n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,(l1 + 1)),(R,(R,b,(m2 + 1)),((m2 + 1),n))] is V15() set
the multF of R . [(R,a,(l1 + 1)),(R,(R,b,(m2 + 1)),((m2 + 1),n))] is set
(R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,b,(m2 + 1)),(R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,b,(m2 + 1)),(R,(R,a,l2),(m2,n))] is V15() set
the multF of R . [(R,b,(m2 + 1)),(R,(R,a,l2),(m2,n))] is set
((R,a,(l1 + 1)) * (R,(R,b,(m2 + 1)),((m2 + 1),n))) + ((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((R,a,(l1 + 1)) * (R,(R,b,(m2 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,a,(l1 + 1)) * (R,(R,b,(m2 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is V15() set
the addF of R . [((R,a,(l1 + 1)) * (R,(R,b,(m2 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is set
(R,b,(m2 + 1)) * (R,a,(l1 + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,b,(m2 + 1)),(R,a,(l1 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,b,(m2 + 1)),(R,a,(l1 + 1))] is V15() set
the multF of R . [(R,b,(m2 + 1)),(R,a,(l1 + 1))] is set
(R,((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . (((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)] is V15() set
(R) . [((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)] is set
(R,((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)) + ((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((R,((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is V15() set
the addF of R . [(R,((R,b,(m2 + 1)) * (R,a,(l1 + 1))),((m2 + 1),n)),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is set
(R,(R,a,(l1 + 1)),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . (((m2 + 1),n),(R,a,(l1 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((m2 + 1),n),(R,a,(l1 + 1))] is V15() set
(R) . [((m2 + 1),n),(R,a,(l1 + 1))] is set
(R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,b,(m2 + 1)),(R,(R,a,(l1 + 1)),((m2 + 1),n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,b,(m2 + 1)),(R,(R,a,(l1 + 1)),((m2 + 1),n))] is V15() set
the multF of R . [(R,b,(m2 + 1)),(R,(R,a,(l1 + 1)),((m2 + 1),n))] is set
((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))) + ((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is V15() set
the addF of R . [((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is set
(R,(R,a,(l1 + 1)),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . ((R,a,(l1 + 1)),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,(l1 + 1)),((m2 + 1),n)] is V15() set
(R) . [(R,a,(l1 + 1)),((m2 + 1),n)] is set
(R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,b,(m2 + 1)),(R,(R,a,(l1 + 1)),((m2 + 1),n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,b,(m2 + 1)),(R,(R,a,(l1 + 1)),((m2 + 1),n))] is V15() set
the multF of R . [(R,b,(m2 + 1)),(R,(R,a,(l1 + 1)),((m2 + 1),n))] is set
((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))) + ((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is V15() set
the addF of R . [((R,b,(m2 + 1)) * (R,(R,a,(l1 + 1)),((m2 + 1),n))),((R,b,(m2 + 1)) * (R,(R,a,l2),(m2,n)))] is set
(R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,l2),(m2,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((R,(R,a,(l1 + 1)),((m2 + 1),n)),(R,(R,a,l2),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,(R,a,(l1 + 1)),((m2 + 1),n)),(R,(R,a,l2),(m2,n))] is V15() set
the addF of R . [(R,(R,a,(l1 + 1)),((m2 + 1),n)),(R,(R,a,l2),(m2,n))] is set
((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,l2),(m2,n))) * (R,b,(m2 + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,l2),(m2,n))),(R,b,(m2 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,l2),(m2,n))),(R,b,(m2 + 1))] is V15() set
the multF of R . [((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,l2),(m2,n))),(R,b,(m2 + 1))] is set
(R,(R,a,(l1 + 1)),(m2,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . ((m2,n),(R,a,(l1 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(m2,n),(R,a,(l1 + 1))] is V15() set
(R) . [(m2,n),(R,a,(l1 + 1))] is set
(R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,(l1 + 1)),(m2,n)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((R,(R,a,(l1 + 1)),((m2 + 1),n)),(R,(R,a,(l1 + 1)),(m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,(R,a,(l1 + 1)),((m2 + 1),n)),(R,(R,a,(l1 + 1)),(m2,n))] is V15() set
the addF of R . [(R,(R,a,(l1 + 1)),((m2 + 1),n)),(R,(R,a,(l1 + 1)),(m2,n))] is set
((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,(l1 + 1)),(m2,n))) * (R,b,(m2 + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . (((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,(l1 + 1)),(m2,n))),(R,b,(m2 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,(l1 + 1)),(m2,n))),(R,b,(m2 + 1))] is V15() set
the multF of R . [((R,(R,a,(l1 + 1)),((m2 + 1),n)) + (R,(R,a,(l1 + 1)),(m2,n))),(R,b,(m2 + 1))] is set
((m2 + 1),n) + (m2,n) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,(l1 + 1)),(((m2 + 1),n) + (m2,n))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . ((((m2 + 1),n) + (m2,n)),(R,a,(l1 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(((m2 + 1),n) + (m2,n)),(R,a,(l1 + 1))] is V15() set
(R) . [(((m2 + 1),n) + (m2,n)),(R,a,(l1 + 1))] is set
(R,(R,a,(l1 + 1)),(((m2 + 1),n) + (m2,n))) * (R,b,(m2 + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,(R,a,(l1 + 1)),(((m2 + 1),n) + (m2,n))),(R,b,(m2 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,(R,a,(l1 + 1)),(((m2 + 1),n) + (m2,n))),(R,b,(m2 + 1))] is V15() set
the multF of R . [(R,(R,a,(l1 + 1)),(((m2 + 1),n) + (m2,n))),(R,b,(m2 + 1))] is set
((m2 + 1),(n + 1)) is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT
(R,(R,a,(l1 + 1)),((m2 + 1),(n + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R) . (((m2 + 1),(n + 1)),(R,a,(l1 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((m2 + 1),(n + 1)),(R,a,(l1 + 1))] is V15() set
(R) . [((m2 + 1),(n + 1)),(R,a,(l1 + 1))] is set
(R,(R,a,(l1 + 1)),((m2 + 1),(n + 1))) * (R,b,(m2 + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,(R,a,(l1 + 1)),((m2 + 1),(n + 1))),(R,b,(m2 + 1))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,(R,a,(l1 + 1)),((m2 + 1),(n + 1))),(R,b,(m2 + 1))] is V15() set
the multF of R . [(R,(R,a,(l1 + 1)),((m2 + 1),(n + 1))),(R,b,(m2 + 1))] is set
(R,a,b,(n + 1)) /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(<*(0. R)*> ^ ((R,a,b,n) * b)) . 1 is set
0 + 1 is non empty V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real positive non negative Element of NAT
Seg (n + 1) is non empty V35() V42(n + 1) Element of bool NAT
(R,a,b,n) . i is set
(((R,a,b,n) * a) ^ <*(0. R)*>) . 1 is set
((R,a,b,n) * a) . 1 is set
((R,a,b,n) * a) /. 1 is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R,a,b,n) /. 1 is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
((R,a,b,n) /. 1) * a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . (((R,a,b,n) /. 1),a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((R,a,b,n) /. 1),a] is V15() set
the multF of R . [((R,a,b,n) /. 1),a] is set
(R,a,n) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (a,n) is set
[a,n] is V15() set
(power R) . [a,n] is set
(R,a,n) * a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((R,a,n),a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(R,a,n),a] is V15() set
the multF of R . [(R,a,n),a] is set
(R,a,(n + 1)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . (a,(n + 1)) is set
[a,(n + 1)] is V15() set
(power R) . [a,(n + 1)] is set
(R,F1,F2) /. i is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(F1 /. i) + (F2 /. i) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((F1 /. i),(F2 /. i)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(F1 /. i),(F2 /. i)] is V15() set
the addF of R . [(F1 /. i),(F2 /. i)] is set
{1} \/ { b₁ where b₁ is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not (n + 1) + 1 <= b₁ ) } is non empty set
({1} \/ { b₁ where b₁ is V24() V25() V26() V30() V31() V32() V33() V35() V40() ext-real non negative Element of NAT : ( not b₁ <= 1 & not (n + 1) + 1 <= b₁ ) } ) \/ {((n + 1) + 1)} is non empty set
(Sum (R,a,b,n)) * (a + b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R is V1() V4([: the carrier of R, the carrier of R:]) V5( the carrier of R) Function-like quasi_total Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . ((Sum (R,a,b,n)),(a + b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum (R,a,b,n)),(a + b)] is V15() set
the multF of R . [(Sum (R,a,b,n)),(a + b)] is set
(Sum (R,a,b,n)) * a is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((Sum (R,a,b,n)),a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum (R,a,b,n)),a] is V15() set
the multF of R . [(Sum (R,a,b,n)),a] is set
(Sum (R,a,b,n)) * b is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the multF of R . ((Sum (R,a,b,n)),b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum (R,a,b,n)),b] is V15() set
the multF of R . [(Sum (R,a,b,n)),b] is set
((Sum (R,a,b,n)) * a) + ((Sum (R,a,b,n)) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . (((Sum (R,a,b,n)) * a),((Sum (R,a,b,n)) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[((Sum (R,a,b,n)) * a),((Sum (R,a,b,n)) * b)] is V15() set
the addF of R . [((Sum (R,a,b,n)) * a),((Sum (R,a,b,n)) * b)] is set
Sum ((R,a,b,n) * a) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(Sum ((R,a,b,n) * a)) + ((Sum (R,a,b,n)) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((Sum ((R,a,b,n) * a)),((Sum (R,a,b,n)) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum ((R,a,b,n) * a)),((Sum (R,a,b,n)) * b)] is V15() set
the addF of R . [(Sum ((R,a,b,n) * a)),((Sum (R,a,b,n)) * b)] is set
Sum ((R,a,b,n) * b) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(Sum ((R,a,b,n) * a)) + (Sum ((R,a,b,n) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((Sum ((R,a,b,n) * a)),(Sum ((R,a,b,n) * b))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum ((R,a,b,n) * a)),(Sum ((R,a,b,n) * b))] is V15() set
the addF of R . [(Sum ((R,a,b,n) * a)),(Sum ((R,a,b,n) * b))] is set
Sum F1 is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
Sum <*(0. R)*> is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(Sum ((R,a,b,n) * a)) + (Sum <*(0. R)*>) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((Sum ((R,a,b,n) * a)),(Sum <*(0. R)*>)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum ((R,a,b,n) * a)),(Sum <*(0. R)*>)] is V15() set
the addF of R . [(Sum ((R,a,b,n) * a)),(Sum <*(0. R)*>)] is set
(Sum ((R,a,b,n) * a)) + (0. R) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((Sum ((R,a,b,n) * a)),(0. R)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum ((R,a,b,n) * a)),(0. R)] is V15() set
the addF of R . [(Sum ((R,a,b,n) * a)),(0. R)] is set
Sum F2 is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(Sum <*(0. R)*>) + (Sum ((R,a,b,n) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((Sum <*(0. R)*>),(Sum ((R,a,b,n) * b))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(Sum <*(0. R)*>),(Sum ((R,a,b,n) * b))] is V15() set
the addF of R . [(Sum <*(0. R)*>),(Sum ((R,a,b,n) * b))] is set
(0. R) + (Sum ((R,a,b,n) * b)) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
the addF of R . ((0. R),(Sum ((R,a,b,n) * b))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
[(0. R),(Sum ((R,a,b,n) * b))] is V15() set
the addF of R . [(0. R),(Sum ((R,a,b,n) * b))] is set
dom F2 is V42((n + 1) + 1) Element of bool NAT
(R,(((R,a,b,n) * a) ^ <*(0. R)*>),(<*(0. R)*> ^ ((R,a,b,n) * b))) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,(((R,a,b,n) * a) ^ <*(0. R)*>),(<*(0. R)*> ^ ((R,a,b,n) * b))) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R,(a + b),0) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(power R) . ((a + b),0) is set
[(a + b),0] is V15() set
(power R) . [(a + b),0] is set
1_ R is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
<*(1_ R)*> is V1() V4( NAT ) V5( the carrier of R) Function-like non empty trivial V35() V42(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum <*(1_ R)*> is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
(R,a,b,0) is V1() V4( NAT ) V5( the carrier of R) Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of R
Sum (R,a,b,0) is left_add-cancelable right_add-cancelable add-cancelable Element of the carrier of R
a is non empty set
R is non empty set
[:R,a:] is set
[:[:R,a:],a:] is set
bool [:[:R,a:],a:] is set
[:NAT,R:] is V35() set
[:[:NAT,R:],a:] is V35() set
bool [:[:NAT,R:],a:] is V35() set
b is Element of a
n is V1() V4([:R,a:]) V5(a) Function-like quasi_total Element of bool [:[:R,a:],a:]
a is non empty set
R is non empty set
[:a,R:] is set
[:[:a,R:],a:] is set
bool [:[:a,R:],a:] is set
[:R,NAT:] is V35() set
[:[:R,NAT:],a:] is V35() set
bool [:[:R,NAT:],a:] is V35() set
b is Element of a
n is V1() V4([:a,R:]) V5(a) Function-like quasi_total Element of bool [:[:a,R:],a:]