:: 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

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

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

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

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

c

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)