:: RATFUNC1 semantic presentation

REAL is V156() V157() V158() V162() set

NAT is non zero epsilon-transitive epsilon-connected ordinal V37() V42() V43() V156() V157() V158() V159() V160() V161() V162() Element of K19(REAL)

K19(REAL) is set

K405() is strict algebraic-closed doubleLoopStr

the carrier of K405() is set

COMPLEX is V156() V162() set

omega is non zero epsilon-transitive epsilon-connected ordinal V37() V42() V43() V156() V157() V158() V159() V160() V161() V162() set

K19(omega) is V37() set

K19(NAT) is V37() set

RAT is V156() V157() V158() V159() V162() set

INT is V156() V157() V158() V159() V160() V162() set

0 is V1() non-empty empty-yielding functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V32() ext-real non positive non negative integer V37() V42() V44( 0 ) FinSequence-like FinSequence-membered V156() V157() V158() V159() V160() V161() V162() set

2 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

K20(NAT,REAL) is V1() set

K19(K20(NAT,REAL)) is set

1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

K244(1,NAT) is M10( NAT )

K20(NAT, the carrier of K405()) is V1() set

K19(K20(NAT, the carrier of K405())) is set

RAT+ is set

{ [b

{ [b

{ [b

K19( { [b

K15(( { [b

3 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

0 is V1() non-empty empty-yielding functional zero epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex V32() ext-real non positive non negative integer V37() V42() V44( 0 ) FinSequence-like FinSequence-membered V136() V156() V157() V158() V159() V160() V161() V162() Element of NAT

Seg 1 is non zero trivial V37() V44(1) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

{1} is non zero trivial V44(1) V156() V157() V158() V159() V160() V161() set

Seg 2 is non zero V37() V44(2) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

{1,2} is non zero V156() V157() V158() V159() V160() V161() set

- 1 is non zero complex V32() ext-real non positive negative integer set

L is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero set

p is Element of the carrier of L

x is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len x is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

z1 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

dom x is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Sum z1 is Element of the carrier of L

Sum x is Element of the carrier of L

p * (Sum x) is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,p,(Sum x)) is Element of the carrier of L

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

z2 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

z2 . (len z1) is Element of the carrier of L

z2 . 0 is Element of the carrier of L

q1 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

q1 . (len x) is Element of the carrier of L

q1 . 0 is Element of the carrier of L

p * (q1 . 0) is Element of the carrier of L

K84( the carrier of L, the multF of L,p,(q1 . 0)) is Element of the carrier of L

q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

z2 . q2 is Element of the carrier of L

q1 . q2 is Element of the carrier of L

p * (q1 . q2) is Element of the carrier of L

K84( the carrier of L, the multF of L,p,(q1 . q2)) is Element of the carrier of L

q2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

z2 . (q2 + 1) is Element of the carrier of L

q1 . (q2 + 1) is Element of the carrier of L

p * (q1 . (q2 + 1)) is Element of the carrier of L

K84( the carrier of L, the multF of L,p,(q1 . (q2 + 1))) is Element of the carrier of L

Seg (len z1) is V37() V44( len z1) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

dom z1 is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Seg (len x) is V37() V44( len x) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

z1 /. (q2 + 1) is Element of the carrier of L

x /. (q2 + 1) is Element of the carrier of L

z1 . (q2 + 1) is set

x . (q2 + 1) is set

(p * (q1 . q2)) + (z1 /. (q2 + 1)) is Element of the carrier of L

the addF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K84( the carrier of L, the addF of L,(p * (q1 . q2)),(z1 /. (q2 + 1))) is Element of the carrier of L

p * (x /. (q2 + 1)) is Element of the carrier of L

K84( the carrier of L, the multF of L,p,(x /. (q2 + 1))) is Element of the carrier of L

(p * (q1 . q2)) + (p * (x /. (q2 + 1))) is Element of the carrier of L

K84( the carrier of L, the addF of L,(p * (q1 . q2)),(p * (x /. (q2 + 1)))) is Element of the carrier of L

(q1 . q2) + (x /. (q2 + 1)) is Element of the carrier of L

K84( the carrier of L, the addF of L,(q1 . q2),(x /. (q2 + 1))) is Element of the carrier of L

p * ((q1 . q2) + (x /. (q2 + 1))) is Element of the carrier of L

K84( the carrier of L, the multF of L,p,((q1 . q2) + (x /. (q2 + 1)))) is Element of the carrier of L

L is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero set

p is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

dom p is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

x is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

x - 1 is complex V32() ext-real integer set

Del (p,x) is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

dom p is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{x} is non zero trivial V44(1) V156() V157() V158() V159() V160() V161() set

(dom p) \ {x} is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Sgm ((dom p) \ {x}) is V1() V4( NAT ) V5( NAT ) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of NAT

p * (Sgm ((dom p) \ {x})) is V1() V4( NAT ) V5( the carrier of L) set

p /. x is Element of the carrier of L

Ins ((Del (p,x)),z1,(p /. x)) is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

(Del (p,x)) | z1 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

Seg z1 is V37() V44(z1) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

K5((Del (p,x)),(Seg z1)) is V1() V4( Seg z1) V4( NAT ) V5( the carrier of L) FinSubsequence-like set

<*(p /. x)*> is V1() V4( NAT ) V5( the carrier of L) Function-like non zero trivial V37() V44(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L

[1,(p /. x)] is V15() set

{[1,(p /. x)]} is V1() non zero trivial V44(1) set

((Del (p,x)) | z1) ^ <*(p /. x)*> is V1() V4( NAT ) V5( the carrier of L) Function-like non zero V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

(Del (p,x)) /^ z1 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

(((Del (p,x)) | z1) ^ <*(p /. x)*>) ^ ((Del (p,x)) /^ z1) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len p is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

len (Del (p,x)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

q1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Seg (q1 + 1) is non zero V37() V44(q1 + 1) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

x - 0 is complex V32() ext-real non negative integer set

len (Ins ((Del (p,x)),z1,(p /. x))) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len (Del (p,x))) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

Seg (len (Ins ((Del (p,x)),z1,(p /. x)))) is V37() V44( len (Ins ((Del (p,x)),z1,(p /. x)))) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

dom (Ins ((Del (p,x)),z1,(p /. x))) is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

q2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(q2 + 1) - 1 is complex V32() ext-real integer set

len ((Del (p,x)) | z1) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Seg (len ((Del (p,x)) | z1)) is V37() V44( len ((Del (p,x)) | z1)) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

dom ((Del (p,x)) | z1) is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Seg (len (Del (p,x))) is V37() V44( len (Del (p,x))) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

dom (Del (p,x)) is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

(Ins ((Del (p,x)),z1,(p /. x))) /. q2 is Element of the carrier of L

(Del (p,x)) /. q2 is Element of the carrier of L

(Del (p,x)) . q2 is set

p . q2 is set

(Ins ((Del (p,x)),z1,(p /. x))) . q2 is set

z1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(Ins ((Del (p,x)),z1,(p /. x))) /. q2 is Element of the carrier of L

(Ins ((Del (p,x)),z1,(p /. x))) . q2 is set

p . q2 is set

q2 - 1 is complex V32() ext-real integer set

(q1 + 1) - 1 is complex V32() ext-real integer set

zz is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

zz + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Seg q1 is V37() V44(q1) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

dom (Del (p,x)) is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

z1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(Ins ((Del (p,x)),z1,(p /. x))) /. (zz + 1) is Element of the carrier of L

(Del (p,x)) /. zz is Element of the carrier of L

(Del (p,x)) . zz is set

p . (zz + 1) is set

p . q2 is set

(Ins ((Del (p,x)),z1,(p /. x))) . q2 is set

(Ins ((Del (p,x)),z1,(p /. x))) . q2 is set

p . q2 is set

(Ins ((Del (p,x)),z1,(p /. x))) . q2 is set

p . q2 is set

L is non empty left_add-cancelable right_add-cancelable right_complementable unital associative commutative right-distributive left-distributive distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero set

p is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

dom p is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Product p is Element of the carrier of L

x is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

p /. x is Element of the carrier of L

Del (p,x) is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

dom p is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{x} is non zero trivial V44(1) V156() V157() V158() V159() V160() V161() set

(dom p) \ {x} is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Sgm ((dom p) \ {x}) is V1() V4( NAT ) V5( NAT ) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of NAT

p * (Sgm ((dom p) \ {x})) is V1() V4( NAT ) V5( the carrier of L) set

Product (Del (p,x)) is Element of the carrier of L

(p /. x) * (Product (Del (p,x))) is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,(p /. x),(Product (Del (p,x)))) is Element of the carrier of L

len p is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Seg (len p) is V37() V44( len p) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

x - 1 is complex V32() ext-real integer set

z2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Ins ((Del (p,x)),z2,(p /. x)) is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

(Del (p,x)) | z2 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

Seg z2 is V37() V44(z2) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

K5((Del (p,x)),(Seg z2)) is V1() V4( Seg z2) V4( NAT ) V5( the carrier of L) FinSubsequence-like set

<*(p /. x)*> is V1() V4( NAT ) V5( the carrier of L) Function-like non zero trivial V37() V44(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of L

[1,(p /. x)] is V15() set

{[1,(p /. x)]} is V1() non zero trivial V44(1) set

((Del (p,x)) | z2) ^ <*(p /. x)*> is V1() V4( NAT ) V5( the carrier of L) Function-like non zero V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

(Del (p,x)) /^ z2 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

(((Del (p,x)) | z2) ^ <*(p /. x)*>) ^ ((Del (p,x)) /^ z2) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

Product (Ins ((Del (p,x)),z2,(p /. x))) is Element of the carrier of L

Product (((Del (p,x)) | z2) ^ <*(p /. x)*>) is Element of the carrier of L

Product ((Del (p,x)) /^ z2) is Element of the carrier of L

(Product (((Del (p,x)) | z2) ^ <*(p /. x)*>)) * (Product ((Del (p,x)) /^ z2)) is Element of the carrier of L

K84( the carrier of L, the multF of L,(Product (((Del (p,x)) | z2) ^ <*(p /. x)*>)),(Product ((Del (p,x)) /^ z2))) is Element of the carrier of L

Product ((Del (p,x)) | z2) is Element of the carrier of L

(Product ((Del (p,x)) | z2)) * (p /. x) is Element of the carrier of L

K84( the carrier of L, the multF of L,(Product ((Del (p,x)) | z2)),(p /. x)) is Element of the carrier of L

((Product ((Del (p,x)) | z2)) * (p /. x)) * (Product ((Del (p,x)) /^ z2)) is Element of the carrier of L

K84( the carrier of L, the multF of L,((Product ((Del (p,x)) | z2)) * (p /. x)),(Product ((Del (p,x)) /^ z2))) is Element of the carrier of L

(Product ((Del (p,x)) | z2)) * (Product ((Del (p,x)) /^ z2)) is Element of the carrier of L

K84( the carrier of L, the multF of L,(Product ((Del (p,x)) | z2)),(Product ((Del (p,x)) /^ z2))) is Element of the carrier of L

(p /. x) * ((Product ((Del (p,x)) | z2)) * (Product ((Del (p,x)) /^ z2))) is Element of the carrier of L

K84( the carrier of L, the multF of L,(p /. x),((Product ((Del (p,x)) | z2)) * (Product ((Del (p,x)) /^ z2)))) is Element of the carrier of L

((Del (p,x)) | z2) ^ ((Del (p,x)) /^ z2) is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

Product (((Del (p,x)) | z2) ^ ((Del (p,x)) /^ z2)) is Element of the carrier of L

(p /. x) * (Product (((Del (p,x)) | z2) ^ ((Del (p,x)) /^ z2))) is Element of the carrier of L

K84( the carrier of L, the multF of L,(p /. x),(Product (((Del (p,x)) | z2) ^ ((Del (p,x)) /^ z2)))) is Element of the carrier of L

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero non trivial set

p is non zero Element of the carrier of L

x is non zero Element of the carrier of L

p / x is Element of the carrier of L

x " is Element of the carrier of L

p * (x ") is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,p,(x ")) is Element of the carrier of L

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

(x ") * x is Element of the carrier of L

K84( the carrier of L, the multF of L,(x "),x) is Element of the carrier of L

1. L is non zero Element of the carrier of L

the OneF of L is Element of the carrier of L

L is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero set

p is Element of the carrier of L

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

x is Element of the carrier of L

p * x is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,p,x) is Element of the carrier of L

z1 is Element of the carrier of L

p * z1 is Element of the carrier of L

K84( the carrier of L, the multF of L,p,z1) is Element of the carrier of L

(p * x) - (p * z1) is Element of the carrier of L

- (p * z1) is Element of the carrier of L

(p * x) + (- (p * z1)) is Element of the carrier of L

the addF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K84( the carrier of L, the addF of L,(p * x),(- (p * z1))) is Element of the carrier of L

x - z1 is Element of the carrier of L

- z1 is Element of the carrier of L

x + (- z1) is Element of the carrier of L

K84( the carrier of L, the addF of L,x,(- z1)) is Element of the carrier of L

p * (x - z1) is Element of the carrier of L

K84( the carrier of L, the multF of L,p,(x - z1)) is Element of the carrier of L

L is non empty left_add-cancelable right_add-cancelable right_complementable left-distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero set

p is Element of the carrier of L

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

x is Element of the carrier of L

x * p is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,x,p) is Element of the carrier of L

z1 is Element of the carrier of L

z1 * p is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,p) is Element of the carrier of L

(x * p) - (z1 * p) is Element of the carrier of L

- (z1 * p) is Element of the carrier of L

(x * p) + (- (z1 * p)) is Element of the carrier of L

the addF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K84( the carrier of L, the addF of L,(x * p),(- (z1 * p))) is Element of the carrier of L

x - z1 is Element of the carrier of L

- z1 is Element of the carrier of L

x + (- z1) is Element of the carrier of L

K84( the carrier of L, the addF of L,x,(- z1)) is Element of the carrier of L

(x - z1) * p is Element of the carrier of L

K84( the carrier of L, the multF of L,(x - z1),p) is Element of the carrier of L

L is complex V32() ext-real integer set

p is complex V32() ext-real integer set

max (L,p) is complex V32() ext-real set

min (L,p) is complex V32() ext-real set

L is complex V32() ext-real integer set

p is complex V32() ext-real integer set

L + p is complex V32() ext-real integer set

x is complex V32() ext-real integer set

L + x is complex V32() ext-real integer set

max ((L + p),(L + x)) is complex V32() ext-real integer set

max (p,x) is complex V32() ext-real integer set

L + (max (p,x)) is complex V32() ext-real integer set

L is non empty ZeroStr

the carrier of L is non zero set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

L is non empty non trivial ZeroStr

the carrier of L is non zero non trivial set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

x is Element of the carrier of L

p is Element of the carrier of L

p is Element of the carrier of L

p is Element of the carrier of L

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

(0_. L) +* (0,p) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

((0_. L) +* (0,p)) . z1 is Element of the carrier of L

(0_. L) . z1 is Element of the carrier of L

z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

((0_. L) +* (0,p)) . z1 is Element of the carrier of L

z2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

z1 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

z2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

dom (0_. L) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

z1 . z2 is Element of the carrier of L

len z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

L is non empty ZeroStr

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

the carrier of L is non zero set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

degree (0_. L) is complex V32() ext-real integer set

len (0_. L) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len (0_. L)) - 1 is complex V32() ext-real integer set

L is non empty non degenerated non trivial multLoopStr_0

1_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

the carrier of L is non zero non trivial set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) (L) Element of K19(K20(NAT, the carrier of L))

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

1. L is non zero Element of the carrier of L

the OneF of L is Element of the carrier of L

(0_. L) +* (0,(1. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

(1_. L) . 0 is Element of the carrier of L

(0_. L) . 0 is Element of the carrier of L

L is non empty multLoopStr_0

1_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

the carrier of L is non zero set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) (L) Element of K19(K20(NAT, the carrier of L))

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

1. L is Element of the carrier of L

the OneF of L is Element of the carrier of L

(0_. L) +* (0,(1. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

dom (1_. L) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

dom (0_. L) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

x is set

z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(0_. L) . z1 is Element of the carrier of L

(1_. L) . x is set

(0_. L) . x is set

x is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

(1_. L) . x is Element of the carrier of L

(0_. L) . x is Element of the carrier of L

x is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

1 + 0 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(1_. L) . 0 is Element of the carrier of L

dom (0_. L) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

len (1_. L) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

degree (1_. L) is complex V32() ext-real integer set

(len (1_. L)) - 1 is complex V32() ext-real integer set

L is non empty ZeroStr

the carrier of L is non zero set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

p is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) (L) Element of K19(K20(NAT, the carrier of L))

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

L is non empty ZeroStr

the carrier of L is non zero set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

p is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

L is non empty non trivial ZeroStr

the carrier of L is non zero non trivial set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

x is Element of the carrier of L

p is Element of the carrier of L

p is Element of the carrier of L

p is Element of the carrier of L

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) (L) Element of K19(K20(NAT, the carrier of L))

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

(0_. L) +* (0,p) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

((0_. L) +* (0,p)) +* (1,p) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

(((0_. L) +* (0,p)) +* (1,p)) . z1 is Element of the carrier of L

((0_. L) +* (0,p)) . z1 is Element of the carrier of L

(0_. L) . z1 is Element of the carrier of L

z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

(((0_. L) +* (0,p)) +* (1,p)) . z1 is Element of the carrier of L

z2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

z1 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

z2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

z1 . z2 is Element of the carrier of L

((0_. L) +* (0,p)) . z2 is Element of the carrier of L

(0_. L) . z2 is Element of the carrier of L

z2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

z1 . 1 is Element of the carrier of L

dom (0_. L) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

dom ((0_. L) +* (0,p)) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

len z1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

degree z1 is complex V32() ext-real integer set

(len z1) - 1 is complex V32() ext-real integer set

L is non empty non degenerated non trivial unital right_unital well-unital left_unital doubleLoopStr

the carrier of L is non zero non trivial set

p is Element of the carrier of L

x is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

rpoly (x,p) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support with_roots (L) (L) Element of K19(K20(NAT, the carrier of L))

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

power L is V1() V4(K20( the carrier of L,NAT)) V5( the carrier of L) Function-like total V18(K20( the carrier of L,NAT), the carrier of L) Element of K19(K20(K20( the carrier of L,NAT), the carrier of L))

K20( the carrier of L,NAT) is V1() V37() set

K20(K20( the carrier of L,NAT), the carrier of L) is V1() V37() set

K19(K20(K20( the carrier of L,NAT), the carrier of L)) is V37() set

K81( the carrier of L,NAT, the carrier of L,(power L),p,x) is Element of the carrier of L

- K81( the carrier of L,NAT, the carrier of L,(power L),p,x) is Element of the carrier of L

1_ L is Element of the carrier of L

1. L is non zero Element of the carrier of L

the OneF of L is Element of the carrier of L

K434( the carrier of L,0,x,(- K81( the carrier of L,NAT, the carrier of L,(power L),p,x)),(1_ L)) is V1() V4({0,x}) V5( the carrier of L) Function-like non zero total V18({0,x}, the carrier of L) Element of K19(K20({0,x}, the carrier of L))

{0,x} is non zero V156() V157() V158() V159() V160() V161() set

K20({0,x}, the carrier of L) is V1() set

K19(K20({0,x}, the carrier of L)) is set

K430((0_. L),K434( the carrier of L,0,x,(- K81( the carrier of L,NAT, the carrier of L,(power L),p,x)),(1_ L))) is V1() Function-like set

degree (rpoly (x,p)) is complex V32() ext-real integer set

len (rpoly (x,p)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len (rpoly (x,p))) - 1 is complex V32() ext-real integer set

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

Polynom-Ring L is non empty left_add-cancelable right_add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

0. (Polynom-Ring L) is zero Element of the carrier of (Polynom-Ring L)

the carrier of (Polynom-Ring L) is non zero set

the ZeroF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) (L) Element of K19(K20(NAT, the carrier of L))

the carrier of L is non zero non trivial set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

1. (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)

the OneF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)

1_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) (L) Element of K19(K20(NAT, the carrier of L))

1. L is non zero Element of the carrier of L

the OneF of L is Element of the carrier of L

(0_. L) +* (0,(1. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

L is non empty non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_cancelable almost_right_cancelable right-distributive left-distributive distributive add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

Polynom-Ring L is non empty left_add-cancelable right_add-cancelable right_complementable strict add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of (Polynom-Ring L) is non zero set

x is Element of the carrier of (Polynom-Ring L)

z1 is Element of the carrier of (Polynom-Ring L)

x * z1 is Element of the carrier of (Polynom-Ring L)

the multF of (Polynom-Ring L) is V1() V4(K20( the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L))) V5( the carrier of (Polynom-Ring L)) Function-like total V18(K20( the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L)), the carrier of (Polynom-Ring L)) Element of K19(K20(K20( the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L)), the carrier of (Polynom-Ring L)))

K20( the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L)) is V1() set

K20(K20( the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L)), the carrier of (Polynom-Ring L)) is V1() set

K19(K20(K20( the carrier of (Polynom-Ring L), the carrier of (Polynom-Ring L)), the carrier of (Polynom-Ring L))) is set

K84( the carrier of (Polynom-Ring L), the multF of (Polynom-Ring L),x,z1) is Element of the carrier of (Polynom-Ring L)

0. (Polynom-Ring L) is zero Element of the carrier of (Polynom-Ring L)

the ZeroF of (Polynom-Ring L) is Element of the carrier of (Polynom-Ring L)

the carrier of L is non zero non trivial set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

z2 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

0_. L is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) (L) Element of K19(K20(NAT, the carrier of L))

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

K464( the carrier of L,NAT,(0. L)) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) T-Sequence-like Element of K19(K20(NAT, the carrier of L))

q1 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

q2 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) Element of K19(K20(NAT, the carrier of L))

degree q2 is complex V32() ext-real integer set

len q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len q2) - 1 is complex V32() ext-real integer set

(len q2) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

0 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

1 - 1 is complex V32() ext-real integer set

(len q2) -' 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) Element of K19(K20(NAT, the carrier of L))

degree q2 is complex V32() ext-real integer set

len q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len q2) - 1 is complex V32() ext-real integer set

(len q2) + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len q2) -' 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len q2) + (len q2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

((len q2) + (len q2)) - 2 is complex V32() ext-real integer set

1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

2 - 2 is complex V32() ext-real integer set

g2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

g2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 *' q2 is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

(q2 *' q2) . g2 is Element of the carrier of L

g2 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len g2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Sum g2 is Element of the carrier of L

dom g2 is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

(((len q2) + (len q2)) - 2) + 1 is complex V32() ext-real integer set

((((len q2) + (len q2)) - 2) + 1) - (len q2) is complex V32() ext-real integer set

p1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

(g2 + 1) -' (len q2) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len q2) + 0 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(len q2) + ((len q2) - 1) is complex V32() ext-real integer set

Seg (len g2) is V37() V44( len g2) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

g2 . (len q2) is set

zz is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() set

q2 . zz is Element of the carrier of L

q2 . p1 is Element of the carrier of L

(q2 . zz) * (q2 . p1) is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,(q2 . zz),(q2 . p1)) is Element of the carrier of L

i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

((len q2) + 1) - 1 is complex V32() ext-real integer set

i - 1 is complex V32() ext-real integer set

i -' 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 . (i -' 1) is Element of the carrier of L

(g2 + 1) -' i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 . ((g2 + 1) -' i) is Element of the carrier of L

(q2 . (i -' 1)) * (q2 . ((g2 + 1) -' i)) is Element of the carrier of L

K84( the carrier of L, the multF of L,(q2 . (i -' 1)),(q2 . ((g2 + 1) -' i))) is Element of the carrier of L

g2 . i is set

(g2 + 1) - i is complex V32() ext-real integer set

(g2 + 1) - (len q2) is complex V32() ext-real integer set

((len q2) - 1) + 1 is complex V32() ext-real integer set

(g2 + 1) -' i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 . ((g2 + 1) -' i) is Element of the carrier of L

i -' 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 . (i -' 1) is Element of the carrier of L

(q2 . (i -' 1)) * (q2 . ((g2 + 1) -' i)) is Element of the carrier of L

K84( the carrier of L, the multF of L,(q2 . (i -' 1)),(q2 . ((g2 + 1) -' i))) is Element of the carrier of L

g2 . i is set

g2 . i is set

g2 . i is set

i is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

g2 /. i is Element of the carrier of L

g2 . i is set

g2 /. (len q2) is Element of the carrier of L

zz + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

p1 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(0_. L) . g2 is Element of the carrier of L

L is non empty left_add-cancelable right_add-cancelable right_complementable associative right-distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

p is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

x is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

p *' x is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

z1 is Element of the carrier of L

z1 * p is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

(z1 * p) *' x is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

z1 * (p *' x) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) Element of K19(K20(NAT, the carrier of L))

dom ((z1 * p) *' x) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

dom (z1 * (p *' x)) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

q2 is set

q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

((z1 * p) *' x) . q2 is set

zz is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len zz is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Sum zz is Element of the carrier of L

dom zz is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

(p *' x) . q2 is set

p1 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len p1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Sum p1 is Element of the carrier of L

dom p1 is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Seg (len p1) is V37() V44( len p1) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

q1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

p1 . q1 is set

p1 /. q1 is Element of the carrier of L

zz /. q1 is Element of the carrier of L

zz . q1 is set

q1 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(z1 * p) . (q1 -' 1) is Element of the carrier of L

(q2 + 1) -' q1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

x . ((q2 + 1) -' q1) is Element of the carrier of L

((z1 * p) . (q1 -' 1)) * (x . ((q2 + 1) -' q1)) is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,((z1 * p) . (q1 -' 1)),(x . ((q2 + 1) -' q1))) is Element of the carrier of L

p . (q1 -' 1) is Element of the carrier of L

z1 * (p . (q1 -' 1)) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,(p . (q1 -' 1))) is Element of the carrier of L

(z1 * (p . (q1 -' 1))) * (x . ((q2 + 1) -' q1)) is Element of the carrier of L

K84( the carrier of L, the multF of L,(z1 * (p . (q1 -' 1))),(x . ((q2 + 1) -' q1))) is Element of the carrier of L

(p . (q1 -' 1)) * (x . ((q2 + 1) -' q1)) is Element of the carrier of L

K84( the carrier of L, the multF of L,(p . (q1 -' 1)),(x . ((q2 + 1) -' q1))) is Element of the carrier of L

z1 * ((p . (q1 -' 1)) * (x . ((q2 + 1) -' q1))) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,((p . (q1 -' 1)) * (x . ((q2 + 1) -' q1)))) is Element of the carrier of L

g2 is Element of the carrier of L

z1 * g2 is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,g2) is Element of the carrier of L

z1 * (p1 /. q1) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,(p1 /. q1)) is Element of the carrier of L

(z1 * (p *' x)) . q2 is Element of the carrier of L

z1 * (Sum p1) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,(Sum p1)) is Element of the carrier of L

((z1 * p) *' x) . q2 is Element of the carrier of L

(z1 * (p *' x)) . q2 is set

L is non empty left_add-cancelable right_add-cancelable right_complementable associative commutative right-distributive left-distributive distributive add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

p is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

x is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

p *' x is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

z1 is Element of the carrier of L

z1 * x is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

p *' (z1 * x) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

z1 * (p *' x) is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

dom (p *' (z1 * x)) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

dom (z1 * (p *' x)) is non zero V156() V157() V158() V159() V160() V161() Element of K19(NAT)

q2 is set

q2 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

q2 + 1 is non zero epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real positive non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(p *' (z1 * x)) . q2 is set

zz is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len zz is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Sum zz is Element of the carrier of L

dom zz is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

(p *' x) . q2 is set

p1 is V1() V4( NAT ) V5( the carrier of L) Function-like V37() FinSequence-like FinSubsequence-like FinSequence of the carrier of L

len p1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

Sum p1 is Element of the carrier of L

dom p1 is V156() V157() V158() V159() V160() V161() Element of K19(NAT)

Seg (len p1) is V37() V44( len p1) V156() V157() V158() V159() V160() V161() Element of K19(NAT)

{ b

q1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

p1 . q1 is set

p1 /. q1 is Element of the carrier of L

zz /. q1 is Element of the carrier of L

zz . q1 is set

q1 -' 1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

p . (q1 -' 1) is Element of the carrier of L

(q2 + 1) -' q1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

(z1 * x) . ((q2 + 1) -' q1) is Element of the carrier of L

(p . (q1 -' 1)) * ((z1 * x) . ((q2 + 1) -' q1)) is Element of the carrier of L

the multF of L is V1() V4(K20( the carrier of L, the carrier of L)) V5( the carrier of L) Function-like total V18(K20( the carrier of L, the carrier of L), the carrier of L) Element of K19(K20(K20( the carrier of L, the carrier of L), the carrier of L))

K20( the carrier of L, the carrier of L) is V1() set

K20(K20( the carrier of L, the carrier of L), the carrier of L) is V1() set

K19(K20(K20( the carrier of L, the carrier of L), the carrier of L)) is set

K84( the carrier of L, the multF of L,(p . (q1 -' 1)),((z1 * x) . ((q2 + 1) -' q1))) is Element of the carrier of L

x . ((q2 + 1) -' q1) is Element of the carrier of L

z1 * (x . ((q2 + 1) -' q1)) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,(x . ((q2 + 1) -' q1))) is Element of the carrier of L

(p . (q1 -' 1)) * (z1 * (x . ((q2 + 1) -' q1))) is Element of the carrier of L

K84( the carrier of L, the multF of L,(p . (q1 -' 1)),(z1 * (x . ((q2 + 1) -' q1)))) is Element of the carrier of L

(p . (q1 -' 1)) * (x . ((q2 + 1) -' q1)) is Element of the carrier of L

K84( the carrier of L, the multF of L,(p . (q1 -' 1)),(x . ((q2 + 1) -' q1))) is Element of the carrier of L

z1 * ((p . (q1 -' 1)) * (x . ((q2 + 1) -' q1))) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,((p . (q1 -' 1)) * (x . ((q2 + 1) -' q1)))) is Element of the carrier of L

g2 is Element of the carrier of L

z1 * g2 is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,g2) is Element of the carrier of L

z1 * (p1 /. q1) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,(p1 /. q1)) is Element of the carrier of L

(z1 * (p *' x)) . q2 is Element of the carrier of L

z1 * (Sum p1) is Element of the carrier of L

K84( the carrier of L, the multF of L,z1,(Sum p1)) is Element of the carrier of L

(p *' (z1 * x)) . q2 is Element of the carrier of L

(z1 * (p *' x)) . q2 is set

L is non empty non degenerated non trivial left_add-cancelable right_add-cancelable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like left_zeroed add-left-invertible add-right-invertible Loop-like doubleLoopStr

the carrier of L is non zero non trivial set

K20(NAT, the carrier of L) is V1() V37() set

K19(K20(NAT, the carrier of L)) is V37() set

p is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support (L) Element of K19(K20(NAT, the carrier of L))

x is non zero Element of the carrier of L

x * p is V1() V4( NAT ) V5( the carrier of L) Function-like non zero total V18( NAT , the carrier of L) finite-Support Element of K19(K20(NAT, the carrier of L))

0. L is zero Element of the carrier of L

the ZeroF of L is Element of the carrier of L

len (x * p) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

len p is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative integer V37() V42() V136() V156() V157() V158() V159() V160() V161() Element of NAT

0_. L is V1() V4( NAT ) V5( the carrier of L)