:: 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₂] where b₁, b₂ 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 omega : ( b₁,b₂ are_relative_prime & not b₂ = 0 ) } is set
{ [b₁,1] where b₁ 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 omega : verum } is set
{ [b₁,b₂] where b₁, b₂ 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 omega : ( b₁,b₂ are_relative_prime & not b₂ = 0 ) } \ { [b₁,1] where b₁ 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 omega : verum } is Element of K19( { [b₁,b₂] where b₁, b₂ 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 omega : ( b₁,b₂ are_relative_prime & not b₂ = 0 ) } )
K19( { [b₁,b₂] where b₁, b₂ 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 omega : ( b₁,b₂ are_relative_prime & not b₂ = 0 ) } ) is set
K15(( { [b₁,b₂] where b₁, b₂ 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 omega : ( b₁,b₂ are_relative_prime & not b₂ = 0 ) } \ { [b₁,1] where b₁ 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 omega : verum } ),omega) is non zero set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= 1 ) } is set
{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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= 2 ) } is set
{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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len z1 ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len x ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= z1 ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= q1 + 1 ) } 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
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len (Ins ((Del (p,x)),z1,(p /. x))) ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len ((Del (p,x)) | z1) ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len (Del (p,x)) ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= q1 ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len p ) } 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
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= z2 ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len g2 ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len p1 ) } is set
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₁ where b₁ 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 : ( 1 <= b₁ & b₁ <= len p1 ) } is set
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)