:: POLYNOM5 semantic presentation

REAL is non empty V24() V56() V57() V58() V62() set
NAT is epsilon-transitive epsilon-connected ordinal non empty V24() V29() V30() V56() V57() V58() V59() V60() V61() V62() Element of K27(REAL)
K27(REAL) is V24() set
INT is non empty V24() V56() V57() V58() V59() V60() V62() set
F_Complex is non empty non degenerated V94() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible strict Abelian add-associative right_zeroed unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital domRing-like V174() V175() V176() V177() doubleLoopStr
the carrier of F_Complex is non empty V19() set
omega is epsilon-transitive epsilon-connected ordinal non empty V24() V29() V30() V56() V57() V58() V59() V60() V61() V62() set
K27(omega) is V24() set
K27(NAT) is V24() set
COMPLEX is non empty V24() V56() V62() set
RAT is non empty V24() V56() V57() V58() V59() V62() set
K28(COMPLEX,COMPLEX) is V24() complex-valued set
K27(K28(COMPLEX,COMPLEX)) is V24() set
K28(COMPLEX,REAL) is V24() complex-valued ext-real-valued real-valued set
K27(K28(COMPLEX,REAL)) is V24() set
K293(NAT) is V78() set
K28(REAL,REAL) is V24() complex-valued ext-real-valued real-valued set
K27(K28(REAL,REAL)) is V24() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
{} is set
the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V24() V29() V31( {} ) FinSequence-membered complex real ext-real non positive non negative V54() V56() V57() V58() V59() V60() V61() V62() set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V24() V29() V31( {} ) FinSequence-membered complex real ext-real non positive non negative V54() V56() V57() V58() V59() V60() V61() V62() set
K28(NAT,REAL) is V24() complex-valued ext-real-valued real-valued set
K27(K28(NAT,REAL)) is V24() set
K250(1,NAT) is M12( NAT )
K28(K28(COMPLEX,COMPLEX),COMPLEX) is V24() complex-valued set
K27(K28(K28(COMPLEX,COMPLEX),COMPLEX)) is V24() set
K28(K28(REAL,REAL),REAL) is V24() complex-valued ext-real-valued real-valued set
K27(K28(K28(REAL,REAL),REAL)) is V24() set
K28(RAT,RAT) is RAT -valued V24() complex-valued ext-real-valued real-valued set
K27(K28(RAT,RAT)) is V24() set
K28(K28(RAT,RAT),RAT) is RAT -valued V24() complex-valued ext-real-valued real-valued set
K27(K28(K28(RAT,RAT),RAT)) is V24() set
K28(INT,INT) is RAT -valued INT -valued V24() complex-valued ext-real-valued real-valued set
K27(K28(INT,INT)) is V24() set
K28(K28(INT,INT),INT) is RAT -valued INT -valued V24() complex-valued ext-real-valued real-valued set
K27(K28(K28(INT,INT),INT)) is V24() set
K28(NAT,NAT) is RAT -valued INT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28(NAT,NAT),NAT) is RAT -valued INT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K27(K28(K28(NAT,NAT),NAT)) is V24() set
3 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
Seg 1 is non empty V19() V24() V31(1) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
{1} is non empty V19() V31(1) V56() V57() V58() V59() V60() V61() set
Seg 2 is non empty V24() V31(2) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
{1,2} is V56() V57() V58() V59() V60() V61() set
Seg 3 is non empty V24() V31(3) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
K97(1,2,3) is V56() V57() V58() V59() V60() V61() set
<*> REAL is Relation-like NAT -defined REAL -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V24() V29() V31( {} ) FinSequence-like FinSubsequence-like FinSequence-membered complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V54() V56() V57() V58() V59() V60() V61() V62() Function-yielding V87() FinSequence of REAL
Sum (<*> REAL) is complex real ext-real Element of REAL
K623() is Relation-like K28(REAL,REAL) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K27(K28(K28(REAL,REAL),REAL))
K294(REAL,(<*> REAL),K623()) is complex real ext-real Element of REAL
K28(NAT,COMPLEX) is V24() complex-valued set
K27(K28(NAT,COMPLEX)) is V24() set
K27(K28(NAT,NAT)) is V24() set
1r is complex Element of COMPLEX
|.0.| is complex real ext-real V55() Element of REAL
|.1r.| is complex real ext-real Element of REAL
K617() is Relation-like K28(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of K27(K28(K28(COMPLEX,COMPLEX),COMPLEX))
K619() is Relation-like K28(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like total quasi_total complex-valued Element of K27(K28(K28(COMPLEX,COMPLEX),COMPLEX))
0c is complex Element of COMPLEX
0. F_Complex is complex zero Element of the carrier of F_Complex
the ZeroF of F_Complex is complex Element of the carrier of F_Complex
1_ F_Complex is complex Element of the carrier of F_Complex
1. F_Complex is complex non zero Element of the carrier of F_Complex
the OneF of F_Complex is complex Element of the carrier of F_Complex
|.(0. F_Complex).| is complex real ext-real Element of REAL
|.(1. F_Complex).| is complex real ext-real Element of REAL
power F_Complex is Relation-like K28( the carrier of F_Complex,NAT) -defined the carrier of F_Complex -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of F_Complex,NAT), the carrier of F_Complex))
K28( the carrier of F_Complex,NAT) is INT -valued RAT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28( the carrier of F_Complex,NAT), the carrier of F_Complex) is V24() set
K27(K28(K28( the carrier of F_Complex,NAT), the carrier of F_Complex)) is V24() set
len {} is epsilon-transitive epsilon-connected ordinal V29() set
c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ * np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(c₁ * np) - c₁ is complex real ext-real V54() Element of REAL
- c₁ is complex real ext-real non positive V54() set
(c₁ * np) + (- c₁) is complex real ext-real V54() set
((c₁ * np) - c₁) - np is complex real ext-real V54() Element of REAL
- np is complex real ext-real non positive V54() set
((c₁ * np) - c₁) + (- np) is complex real ext-real V54() set
(((c₁ * np) - c₁) - np) + 1 is complex real ext-real V54() Element of REAL
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(0 + 1) - 1 is complex real ext-real V54() Element of REAL
- 1 is non empty complex real ext-real non positive negative V54() set
(0 + 1) + (- 1) is complex real ext-real V54() set
np - 1 is complex real ext-real V54() Element of REAL
np + (- 1) is complex real ext-real V54() set
c₁ - 1 is complex real ext-real V54() Element of REAL
c₁ + (- 1) is complex real ext-real V54() set
(c₁ - 1) * (np - 1) is complex real ext-real V54() Element of REAL
np is complex real ext-real set
c₁ is complex real ext-real set
min (c₁,np) is complex real ext-real set
max (c₁,np) is complex real ext-real set
(min (c₁,np)) / (max (c₁,np)) is complex real ext-real Element of COMPLEX
(max (c₁,np)) " is complex real ext-real set
(min (c₁,np)) * ((max (c₁,np)) ") is complex real ext-real set
np is complex real ext-real set
c₁ is complex real ext-real set
max (c₁,np) is complex real ext-real set
min (c₁,np) is complex real ext-real set
2 * (max (c₁,np)) is complex real ext-real Element of REAL
(min (c₁,np)) / (2 * (max (c₁,np))) is complex real ext-real Element of REAL
(2 * (max (c₁,np))) " is complex real ext-real set
(min (c₁,np)) * ((2 * (max (c₁,np))) ") is complex real ext-real set
np * 2 is complex real ext-real Element of REAL
(min (c₁,np)) / (max (c₁,np)) is complex real ext-real Element of COMPLEX
(max (c₁,np)) " is complex real ext-real set
(min (c₁,np)) * ((max (c₁,np)) ") is complex real ext-real set
((min (c₁,np)) / (max (c₁,np))) * 2 is complex real ext-real Element of REAL
((min (c₁,np)) / (max (c₁,np))) / 2 is complex real ext-real Element of REAL
2 " is non empty complex real ext-real positive non negative set
((min (c₁,np)) / (max (c₁,np))) * (2 ") is complex real ext-real set
(max (c₁,np)) * 2 is complex real ext-real Element of REAL
(min (c₁,np)) / ((max (c₁,np)) * 2) is complex real ext-real Element of REAL
((max (c₁,np)) * 2) " is complex real ext-real set
(min (c₁,np)) * (((max (c₁,np)) * 2) ") is complex real ext-real set
((min (c₁,np)) / (2 * (max (c₁,np)))) * c₁ is complex real ext-real Element of REAL
np / 2 is complex real ext-real Element of REAL
np * (2 ") is complex real ext-real set
2 * np is complex real ext-real Element of REAL
c₁ / (2 * np) is complex real ext-real Element of REAL
(2 * np) " is complex real ext-real set
c₁ * ((2 * np) ") is complex real ext-real set
(c₁ / (2 * np)) * np is complex real ext-real Element of REAL
c₁ / 2 is complex real ext-real Element of REAL
c₁ * (2 ") is complex real ext-real set
np / 2 is complex real ext-real Element of REAL
np * (2 ") is complex real ext-real set
1 / 2 is non empty complex real ext-real positive non negative Element of REAL
2 " is non empty complex real ext-real positive non negative set
1 * (2 ") is non empty complex real ext-real positive non negative set
(1 / 2) * c₁ is complex real ext-real Element of REAL
np is complex real ext-real Element of REAL
c₁ is complex real ext-real Element of REAL
z0 is complex real ext-real set
z0 * c₁ is complex real ext-real Element of REAL
c₁ is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom c₁ is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
Sum c₁ is complex real ext-real Element of REAL
K294(REAL,c₁,K623()) is complex real ext-real Element of REAL
np is complex real ext-real Element of REAL
<*np*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
c₁ ^ <*np*> is Relation-like NAT -defined REAL -valued Function-like non empty V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom (c₁ ^ <*np*>) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
Sum (c₁ ^ <*np*>) is complex real ext-real Element of REAL
K294(REAL,(c₁ ^ <*np*>),K623()) is complex real ext-real Element of REAL
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(c₁ ^ <*np*>) . z0 is complex real ext-real Element of REAL
c₁ . z0 is complex real ext-real Element of REAL
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ | z0 is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (c₁ | z0) is complex real ext-real Element of REAL
K294(REAL,(c₁ | z0),K623()) is complex real ext-real Element of REAL
z0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ | (z0 + 1) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (c₁ | (z0 + 1)) is complex real ext-real Element of REAL
K294(REAL,(c₁ | (z0 + 1)),K623()) is complex real ext-real Element of REAL
len c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ /. (z0 + 1) is complex real ext-real Element of REAL
<*(c₁ /. (z0 + 1))*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
(c₁ | z0) ^ <*(c₁ /. (z0 + 1))*> is Relation-like NAT -defined REAL -valued Function-like non empty V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(Sum (c₁ | z0)) + (c₁ /. (z0 + 1)) is complex real ext-real Element of REAL
c₁ . (z0 + 1) is complex real ext-real Element of REAL
len c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(c₁ ^ <*np*>) . z0 is complex real ext-real Element of REAL
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(len c₁) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len (c₁ ^ <*np*>) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(c₁ ^ <*np*>) . (len (c₁ ^ <*np*>)) is complex real ext-real Element of REAL
(c₁ ^ <*np*>) . ((len c₁) + 1) is complex real ext-real Element of REAL
c₁ . z0 is complex real ext-real Element of REAL
(c₁ . z0) + 0 is complex real ext-real Element of REAL
(c₁ . z0) + np is complex real ext-real Element of REAL
c₁ | (len c₁) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Seg ((len c₁) + 1) is non empty V24() V31((len c₁) + 1) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
Seg (len c₁) is V24() V31( len c₁) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
{((len c₁) + 1)} is non empty V19() V31(1) V56() V57() V58() V59() V60() V61() Element of K27(REAL)
(Seg (len c₁)) \/ {((len c₁) + 1)} is V56() V57() V58() V59() V60() V61() set
(dom c₁) \/ {((len c₁) + 1)} is V56() V57() V58() V59() V60() V61() set
c₁ | 0 is Relation-like NAT -defined REAL -valued RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V24() V29() V31( {} ) FinSequence-like FinSubsequence-like FinSequence-membered complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V54() V56() V57() V58() V59() V60() V61() V62() Function-yielding V87() FinSequence of REAL
Sum (c₁ | 0) is complex real ext-real Element of REAL
K294(REAL,(c₁ | 0),K623()) is complex real ext-real Element of REAL
(Sum c₁) + np is complex real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ . k is complex real ext-real Element of REAL
0 + ((c₁ ^ <*np*>) . z0) is complex real ext-real Element of REAL
(Sum c₁) + np is complex real ext-real Element of REAL
dom (<*> REAL) is epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() Element of K27(NAT)
c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(<*> REAL) . c₁ is Relation-like epsilon-transitive epsilon-connected ordinal natural Function-like V24() V29() complex real ext-real non negative V54() Element of REAL
c₁ is complex real ext-real Element of REAL
np is complex real ext-real Element of REAL
[**c₁,np**] is complex Element of the carrier of F_Complex
<i> is complex Element of COMPLEX
K286(REAL,0,1,0,1) is Relation-like {0,1} -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K27(K28({0,1},REAL))
{0,1} is V56() V57() V58() V59() V60() V61() set
K28({0,1},REAL) is complex-valued ext-real-valued real-valued set
K27(K28({0,1},REAL)) is set
np * <i> is complex set
c₁ + (np * <i>) is complex set
- [**c₁,np**] is complex Element of the carrier of F_Complex
- c₁ is complex real ext-real Element of REAL
- np is complex real ext-real Element of REAL
[**(- c₁),(- np)**] is complex Element of the carrier of F_Complex
(- np) * <i> is complex set
(- c₁) + ((- np) * <i>) is complex set
- (c₁ + (np * <i>)) is complex set
c₁ is complex real ext-real Element of REAL
np is complex real ext-real Element of REAL
[**c₁,np**] is complex Element of the carrier of F_Complex
<i> is complex Element of COMPLEX
K286(REAL,0,1,0,1) is Relation-like {0,1} -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K27(K28({0,1},REAL))
{0,1} is V56() V57() V58() V59() V60() V61() set
K28({0,1},REAL) is complex-valued ext-real-valued real-valued set
K27(K28({0,1},REAL)) is set
np * <i> is complex set
c₁ + (np * <i>) is complex set
z0 is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
[**z0,k**] is complex Element of the carrier of F_Complex
k * <i> is complex set
z0 + (k * <i>) is complex set
[**c₁,np**] - [**z0,k**] is complex Element of the carrier of F_Complex
- [**z0,k**] is complex Element of the carrier of F_Complex
[**c₁,np**] + (- [**z0,k**]) is complex Element of the carrier of F_Complex
the addF of F_Complex is Relation-like K28( the carrier of F_Complex, the carrier of F_Complex) -defined the carrier of F_Complex -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex))
K28( the carrier of F_Complex, the carrier of F_Complex) is set
K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex) is set
K27(K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex)) is set
the addF of F_Complex . ([**c₁,np**],(- [**z0,k**])) is complex Element of the carrier of F_Complex
K593([**c₁,np**],(- [**z0,k**])) is complex Element of COMPLEX
c₁ - z0 is complex real ext-real Element of REAL
- z0 is complex real ext-real set
c₁ + (- z0) is complex real ext-real set
np - k is complex real ext-real Element of REAL
- k is complex real ext-real set
np + (- k) is complex real ext-real set
[**(c₁ - z0),(np - k)**] is complex Element of the carrier of F_Complex
(np - k) * <i> is complex set
(c₁ - z0) + ((np - k) * <i>) is complex set
- z0 is complex real ext-real Element of REAL
- k is complex real ext-real Element of REAL
[**(- z0),(- k)**] is complex Element of the carrier of F_Complex
(- k) * <i> is complex set
(- z0) + ((- k) * <i>) is complex set
[**c₁,np**] + [**(- z0),(- k)**] is complex Element of the carrier of F_Complex
the addF of F_Complex . ([**c₁,np**],[**(- z0),(- k)**]) is complex Element of the carrier of F_Complex
K593([**c₁,np**],[**(- z0),(- k)**]) is complex Element of COMPLEX
c₁ is complex Element of the carrier of F_Complex
|.c₁.| is complex real ext-real Element of REAL
np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power F_Complex) . (c₁,np) is complex Element of the carrier of F_Complex
|.((power F_Complex) . (c₁,np)).| is complex real ext-real Element of REAL
|.c₁.| to_power np is complex real ext-real Element of REAL
np + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power F_Complex) . (c₁,(np + 1)) is complex Element of the carrier of F_Complex
|.((power F_Complex) . (c₁,(np + 1))).| is complex real ext-real Element of REAL
|.c₁.| to_power (np + 1) is complex real ext-real Element of REAL
((power F_Complex) . (c₁,np)) * c₁ is complex Element of the carrier of F_Complex
the multF of F_Complex is Relation-like K28( the carrier of F_Complex, the carrier of F_Complex) -defined the carrier of F_Complex -valued Function-like total quasi_total associative Element of K27(K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex))
K28( the carrier of F_Complex, the carrier of F_Complex) is set
K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex) is set
K27(K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex)) is set
the multF of F_Complex . (((power F_Complex) . (c₁,np)),c₁) is complex Element of the carrier of F_Complex
K595(((power F_Complex) . (c₁,np)),c₁) is complex Element of COMPLEX
|.(((power F_Complex) . (c₁,np)) * c₁).| is complex real ext-real Element of REAL
(|.c₁.| to_power np) * |.c₁.| is complex real ext-real Element of REAL
|.c₁.| to_power 1 is complex real ext-real Element of REAL
(|.c₁.| to_power np) * (|.c₁.| to_power 1) is complex real ext-real Element of REAL
(power F_Complex) . (c₁,0) is complex Element of the carrier of F_Complex
|.((power F_Complex) . (c₁,0)).| is complex real ext-real Element of REAL
|.c₁.| to_power 0 is complex real ext-real Element of REAL
c₁ is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
len c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
dom c₁ is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
np is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
dom np is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
np /. z0 is complex real ext-real Element of REAL
c₁ /. z0 is complex Element of the carrier of F_Complex
|.(c₁ /. z0).| is complex real ext-real Element of REAL
np is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
z0 is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
k is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set
np /. k is complex real ext-real Element of REAL
c₁ /. k is complex Element of the carrier of F_Complex
|.(c₁ /. k).| is complex real ext-real Element of REAL
z0 /. k is complex real ext-real Element of REAL
dom np is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
dom z0 is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
<*> the carrier of F_Complex is Relation-like NAT -defined the carrier of F_Complex -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty V24() V29() V31( {} ) FinSequence-like FinSubsequence-like FinSequence-membered complex real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V54() V56() V57() V58() V59() V60() V61() V62() Function-yielding V87() FinSequence of the carrier of F_Complex
((<*> the carrier of F_Complex)) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len ((<*> the carrier of F_Complex)) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len (<*> the carrier of F_Complex) is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V24() V29() V31( {} ) FinSequence-membered complex real ext-real non positive non negative V54() V55() V56() V57() V58() V59() V60() V61() V62() Element of NAT
c₁ is complex Element of the carrier of F_Complex
<*c₁*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
(<*c₁*>) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
|.c₁.| is complex real ext-real Element of REAL
<*|.c₁.|*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
Seg (0 + 1) is non empty V24() V31(0 + 1) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
dom <*c₁*> is non empty V19() V31(1) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
len (<*c₁*>) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len <*c₁*> is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
dom (<*c₁*>) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set
(<*c₁*>) . np is complex real ext-real Element of REAL
(<*c₁*>) /. 1 is complex real ext-real Element of REAL
<*c₁*> /. 1 is complex Element of the carrier of F_Complex
|.(<*c₁*> /. 1).| is complex real ext-real Element of REAL
<*|.c₁.|*> . np is complex real ext-real Element of REAL
len <*|.c₁.|*> is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ is complex Element of the carrier of F_Complex
np is complex Element of the carrier of F_Complex
<*c₁,np*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like M13( the carrier of F_Complex,K250(2, the carrier of F_Complex))
K250(2, the carrier of F_Complex) is M12( the carrier of F_Complex)
(<*c₁,np*>) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
|.c₁.| is complex real ext-real Element of REAL
|.np.| is complex real ext-real Element of REAL
<*|.c₁.|,|.np.|*> is Relation-like NAT -defined REAL -valued Function-like non empty V24() V31(2) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued M13( REAL ,K250(2,REAL))
K250(2,REAL) is M12( REAL )
len (<*c₁,np*>) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len <*c₁,np*> is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
dom (<*c₁,np*>) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set
dom <*c₁,np*> is V31(2) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
(<*c₁,np*>) . 1 is complex real ext-real Element of REAL
(<*c₁,np*>) /. 1 is complex real ext-real Element of REAL
<*c₁,np*> /. 1 is complex Element of the carrier of F_Complex
|.(<*c₁,np*> /. 1).| is complex real ext-real Element of REAL
(<*c₁,np*>) . z0 is complex real ext-real Element of REAL
<*|.c₁.|,|.np.|*> . z0 is complex real ext-real Element of REAL
dom <*c₁,np*> is V31(2) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
(<*c₁,np*>) . 2 is complex real ext-real Element of REAL
(<*c₁,np*>) /. 2 is complex real ext-real Element of REAL
<*c₁,np*> /. 2 is complex Element of the carrier of F_Complex
|.(<*c₁,np*> /. 2).| is complex real ext-real Element of REAL
(<*c₁,np*>) . z0 is complex real ext-real Element of REAL
<*|.c₁.|,|.np.|*> . z0 is complex real ext-real Element of REAL
len <*|.c₁.|,|.np.|*> is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ is complex Element of the carrier of F_Complex
np is complex Element of the carrier of F_Complex
z0 is complex Element of the carrier of F_Complex
<*c₁,np,z0*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
(<*c₁,np,z0*>) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
|.c₁.| is complex real ext-real Element of REAL
|.np.| is complex real ext-real Element of REAL
|.z0.| is complex real ext-real Element of REAL
<*|.c₁.|,|.np.|,|.z0.|*> is Relation-like NAT -defined REAL -valued Function-like non empty V24() V31(3) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (<*c₁,np,z0*>) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len <*c₁,np,z0*> is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
dom (<*c₁,np,z0*>) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
k is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set
dom <*c₁,np,z0*> is V31(3) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
(<*c₁,np,z0*>) . 1 is complex real ext-real Element of REAL
(<*c₁,np,z0*>) /. 1 is complex real ext-real Element of REAL
<*c₁,np,z0*> /. 1 is complex Element of the carrier of F_Complex
|.(<*c₁,np,z0*> /. 1).| is complex real ext-real Element of REAL
(<*c₁,np,z0*>) . k is complex real ext-real Element of REAL
<*|.c₁.|,|.np.|,|.z0.|*> . k is complex real ext-real Element of REAL
dom <*c₁,np,z0*> is V31(3) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
(<*c₁,np,z0*>) . 2 is complex real ext-real Element of REAL
(<*c₁,np,z0*>) /. 2 is complex real ext-real Element of REAL
<*c₁,np,z0*> /. 2 is complex Element of the carrier of F_Complex
|.(<*c₁,np,z0*> /. 2).| is complex real ext-real Element of REAL
(<*c₁,np,z0*>) . k is complex real ext-real Element of REAL
<*|.c₁.|,|.np.|,|.z0.|*> . k is complex real ext-real Element of REAL
dom <*c₁,np,z0*> is V31(3) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
(<*c₁,np,z0*>) . 3 is complex real ext-real Element of REAL
(<*c₁,np,z0*>) /. 3 is complex real ext-real Element of REAL
<*c₁,np,z0*> /. 3 is complex Element of the carrier of F_Complex
|.(<*c₁,np,z0*> /. 3).| is complex real ext-real Element of REAL
(<*c₁,np,z0*>) . k is complex real ext-real Element of REAL
<*|.c₁.|,|.np.|,|.z0.|*> . k is complex real ext-real Element of REAL
len <*|.c₁.|,|.np.|,|.z0.|*> is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
np is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
c₁ ^ np is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
((c₁ ^ np)) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(c₁) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(np) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(c₁) ^ (np) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom ((c₁ ^ np)) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
len ((c₁ ^ np)) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
Seg (len ((c₁ ^ np))) is V24() V31( len ((c₁ ^ np))) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
len (c₁) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len c₁ is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set
len (c₁ ^ np) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
dom (c₁ ^ np) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
dom c₁ is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
(c₁ ^ np) /. z0 is complex Element of the carrier of F_Complex
(c₁ ^ np) . z0 is set
c₁ . z0 is set
c₁ /. z0 is complex Element of the carrier of F_Complex
dom (c₁) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
((c₁ ^ np)) . z0 is complex real ext-real Element of REAL
((c₁ ^ np)) /. z0 is complex real ext-real Element of REAL
|.((c₁ ^ np) /. z0).| is complex real ext-real Element of REAL
(c₁) /. z0 is complex real ext-real Element of REAL
(c₁) . z0 is complex real ext-real Element of REAL
((c₁) ^ (np)) . z0 is complex real ext-real Element of REAL
dom c₁ is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
0 + (len c₁) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
z0 - (len c₁) is complex real ext-real V54() Element of REAL
- (len c₁) is complex real ext-real non positive V54() set
z0 + (- (len c₁)) is complex real ext-real V54() set
(len c₁) + (z0 - (len c₁)) is complex real ext-real V54() Element of REAL
z0 -' (len c₁) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(len c₁) + (z0 -' (len c₁)) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(len np) + (len c₁) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
1 + (len c₁) is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
Seg (len np) is V24() V31( len np) V56() V57() V58() V59() V60() V61() Element of K27(NAT)
dom np is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
len (np) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
dom (np) is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
(c₁ ^ np) /. z0 is complex Element of the carrier of F_Complex
(c₁ ^ np) . z0 is set
np . (z0 -' (len c₁)) is set
np /. (z0 -' (len c₁)) is complex Element of the carrier of F_Complex
((c₁ ^ np)) . z0 is complex real ext-real Element of REAL
((c₁ ^ np)) /. z0 is complex real ext-real Element of REAL
|.((c₁ ^ np) /. z0).| is complex real ext-real Element of REAL
(np) /. (z0 -' (len c₁)) is complex real ext-real Element of REAL
(np) . (z0 -' (len c₁)) is complex real ext-real Element of REAL
((c₁) ^ (np)) . z0 is complex real ext-real Element of REAL
dom c₁ is V56() V57() V58() V59() V60() V61() Element of K27(NAT)
len np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(len c₁) + (len np) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len (np) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(len c₁) + (len (np)) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(len (c₁)) + (len (np)) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
len ((c₁) ^ (np)) is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
c₁ is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
(c₁) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
np is complex Element of the carrier of F_Complex
<*np*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
c₁ ^ <*np*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
((c₁ ^ <*np*>)) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
|.np.| is complex real ext-real Element of REAL
<*|.np.|*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
(c₁) ^ <*|.np.|*> is Relation-like NAT -defined REAL -valued Function-like non empty V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
<*np*> ^ c₁ is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
((<*np*> ^ c₁)) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
<*|.np.|*> ^ (c₁) is Relation-like NAT -defined REAL -valued Function-like non empty V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(<*np*>) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(c₁) ^ (<*np*>) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(<*np*>) ^ (c₁) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
np is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
Sum np is complex Element of the carrier of F_Complex
|.(Sum np).| is complex real ext-real Element of REAL
(np) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (np) is complex real ext-real Element of REAL
K294(REAL,(np),K623()) is complex real ext-real Element of REAL
z0 is complex Element of the carrier of F_Complex
|.z0.| is complex real ext-real Element of REAL
|.(Sum np).| + |.z0.| is complex real ext-real Element of REAL
(Sum (np)) + |.z0.| is complex real ext-real Element of REAL
<*z0*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
np ^ <*z0*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V24() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex
Sum (np ^ <*z0*>) is complex Element of the carrier of F_Complex
(Sum np) + z0 is complex Element of the carrier of F_Complex
the addF of F_Complex is Relation-like K28( the carrier of F_Complex, the carrier of F_Complex) -defined the carrier of F_Complex -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex))
K28( the carrier of F_Complex, the carrier of F_Complex) is set
K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex) is set
K27(K28(K28( the carrier of F_Complex, the carrier of F_Complex), the carrier of F_Complex)) is set
the addF of F_Complex . ((Sum np),z0) is complex Element of the carrier of F_Complex
K593((Sum np),z0) is complex Element of COMPLEX
|.(Sum (np ^ <*z0*>)).| is complex real ext-real Element of REAL
<*|.z0.|*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty V19() V24() V31(1) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
Sum <*|.z0.|*> is complex real ext-real Element of REAL
K294(REAL,<*|.z0.|*>,K623()) is complex real ext-real Element of REAL
(Sum (np)) + (Sum <*|.z0.|*>) is complex real ext-real Element of REAL
(<*z0*>) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (<*z0*>) is complex real ext-real Element of REAL
K294(REAL,(<*z0*>),K623()) is complex real ext-real Element of REAL
(Sum (np)) + (Sum (<*z0*>)) is complex real ext-real Element of REAL
(np) ^ (<*z0*>) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum ((np) ^ (<*z0*>)) is complex real ext-real Element of REAL
K294(REAL,((np) ^ (<*z0*>)),K623()) is complex real ext-real Element of REAL
((np ^ <*z0*>)) is Relation-like NAT -defined REAL -valued Function-like V24() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum ((np ^ <*z0*>)) is complex real ext-real Element of REAL
K294(REAL,((np ^ <*z0*>)),K623()) is complex real ext-real Element of REAL
Sum (<*> the carrier of F_Complex) is complex Element of the carrier of F_Complex
|.(Sum (<*> the carrier of F_Complex)).| is complex real ext-real Element of REAL
Sum ((<*> the carrier of F_Complex)) is complex real ext-real Element of REAL
K294(REAL,((<*> the carrier of F_Complex)),K623()) is complex real ext-real Element of REAL
c₁ is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed commutative right-distributive left-distributive right_unital distributive V174() V175() V176() V177() doubleLoopStr
the carrier of c₁ is non empty set
K28(NAT, the carrier of c₁) is V24() set
K27(K28(NAT, the carrier of c₁)) is V24() set
Polynom-Ring c₁ is non empty left_add-cancelable right_add-cancelable right_complementable strict Abelian add-associative right_zeroed commutative right-distributive left-distributive distributive V174() V175() V176() V177() doubleLoopStr
power (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁),NAT) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)))
the carrier of (Polynom-Ring c₁) is non empty set
K28( the carrier of (Polynom-Ring c₁),NAT) is INT -valued RAT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)) is V24() set
K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁))) is V24() set
np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power (Polynom-Ring c₁)) . (np,z0) is set
k is Element of the carrier of (Polynom-Ring c₁)
(power (Polynom-Ring c₁)) . (k,z0) is Element of the carrier of (Polynom-Ring c₁)
c₁ is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed commutative right-distributive left-distributive right_unital distributive V174() V175() V176() V177() doubleLoopStr
the carrier of c₁ is non empty set
K28(NAT, the carrier of c₁) is V24() set
K27(K28(NAT, the carrier of c₁)) is V24() set
np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(c₁,np,z0) is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total Element of K27(K28(NAT, the carrier of c₁))
Polynom-Ring c₁ is non empty left_add-cancelable right_add-cancelable right_complementable strict Abelian add-associative right_zeroed commutative right-distributive left-distributive distributive V174() V175() V176() V177() doubleLoopStr
power (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁),NAT) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)))
the carrier of (Polynom-Ring c₁) is non empty set
K28( the carrier of (Polynom-Ring c₁),NAT) is INT -valued RAT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)) is V24() set
K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁))) is V24() set
(power (Polynom-Ring c₁)) . (np,z0) is set
k is Element of the carrier of (Polynom-Ring c₁)
(power (Polynom-Ring c₁)) . (k,z0) is Element of the carrier of (Polynom-Ring c₁)
c₁ is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
the carrier of c₁ is non empty set
K28(NAT, the carrier of c₁) is V24() set
K27(K28(NAT, the carrier of c₁)) is V24() set
1_. c₁ is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
0_. c₁ is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
0. c₁ is zero Element of the carrier of c₁
the ZeroF of c₁ is Element of the carrier of c₁
NAT --> (0. c₁) is Relation-like NAT -defined the carrier of c₁ -valued T-Sequence-like Function-like constant non empty total quasi_total Element of K27(K28(NAT, the carrier of c₁))
1. c₁ is Element of the carrier of c₁
the OneF of c₁ is Element of the carrier of c₁
(0_. c₁) +* (0,(1. c₁)) is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total Element of K27(K28(NAT, the carrier of c₁))
np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
(c₁,np,0) is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
Polynom-Ring c₁ is non empty left_add-cancelable right_add-cancelable right_complementable strict Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
power (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁),NAT) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)))
the carrier of (Polynom-Ring c₁) is non empty set
K28( the carrier of (Polynom-Ring c₁),NAT) is INT -valued RAT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)) is V24() set
K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁))) is V24() set
(power (Polynom-Ring c₁)) . (np,0) is set
z0 is Element of the carrier of (Polynom-Ring c₁)
(power (Polynom-Ring c₁)) . (z0,0) is Element of the carrier of (Polynom-Ring c₁)
1_ (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
1. (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
the OneF of (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
c₁ is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
the carrier of c₁ is non empty set
K28(NAT, the carrier of c₁) is V24() set
K27(K28(NAT, the carrier of c₁)) is V24() set
np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
(c₁,np,1) is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
Polynom-Ring c₁ is non empty left_add-cancelable right_add-cancelable right_complementable strict Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
power (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁),NAT) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)))
the carrier of (Polynom-Ring c₁) is non empty set
K28( the carrier of (Polynom-Ring c₁),NAT) is INT -valued RAT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)) is V24() set
K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁))) is V24() set
(power (Polynom-Ring c₁)) . (np,1) is set
z0 is Element of the carrier of (Polynom-Ring c₁)
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power (Polynom-Ring c₁)) . (z0,(0 + 1)) is Element of the carrier of (Polynom-Ring c₁)
(power (Polynom-Ring c₁)) . (z0,0) is Element of the carrier of (Polynom-Ring c₁)
((power (Polynom-Ring c₁)) . (z0,0)) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁)))
K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)) is set
K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁)) is set
K27(K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁))) is set
the multF of (Polynom-Ring c₁) . (((power (Polynom-Ring c₁)) . (z0,0)),z0) is Element of the carrier of (Polynom-Ring c₁)
1_ (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
1. (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
the OneF of (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
(1_ (Polynom-Ring c₁)) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . ((1_ (Polynom-Ring c₁)),z0) is Element of the carrier of (Polynom-Ring c₁)
c₁ is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
the carrier of c₁ is non empty set
K28(NAT, the carrier of c₁) is V24() set
K27(K28(NAT, the carrier of c₁)) is V24() set
np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
(c₁,np,2) is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
Polynom-Ring c₁ is non empty left_add-cancelable right_add-cancelable right_complementable strict Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
power (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁),NAT) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)))
the carrier of (Polynom-Ring c₁) is non empty set
K28( the carrier of (Polynom-Ring c₁),NAT) is INT -valued RAT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)) is V24() set
K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁))) is V24() set
(power (Polynom-Ring c₁)) . (np,2) is set
np *' np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
z0 is Element of the carrier of (Polynom-Ring c₁)
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power (Polynom-Ring c₁)) . (z0,(1 + 1)) is Element of the carrier of (Polynom-Ring c₁)
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power (Polynom-Ring c₁)) . (z0,(0 + 1)) is Element of the carrier of (Polynom-Ring c₁)
((power (Polynom-Ring c₁)) . (z0,(0 + 1))) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁)))
K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)) is set
K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁)) is set
K27(K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁))) is set
the multF of (Polynom-Ring c₁) . (((power (Polynom-Ring c₁)) . (z0,(0 + 1))),z0) is Element of the carrier of (Polynom-Ring c₁)
(power (Polynom-Ring c₁)) . (z0,0) is Element of the carrier of (Polynom-Ring c₁)
((power (Polynom-Ring c₁)) . (z0,0)) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (((power (Polynom-Ring c₁)) . (z0,0)),z0) is Element of the carrier of (Polynom-Ring c₁)
(((power (Polynom-Ring c₁)) . (z0,0)) * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . ((((power (Polynom-Ring c₁)) . (z0,0)) * z0),z0) is Element of the carrier of (Polynom-Ring c₁)
1_ (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
1. (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
the OneF of (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
(1_ (Polynom-Ring c₁)) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . ((1_ (Polynom-Ring c₁)),z0) is Element of the carrier of (Polynom-Ring c₁)
((1_ (Polynom-Ring c₁)) * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (((1_ (Polynom-Ring c₁)) * z0),z0) is Element of the carrier of (Polynom-Ring c₁)
z0 * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (z0,z0) is Element of the carrier of (Polynom-Ring c₁)
c₁ is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
the carrier of c₁ is non empty set
K28(NAT, the carrier of c₁) is V24() set
K27(K28(NAT, the carrier of c₁)) is V24() set
np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
(c₁,np,3) is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
Polynom-Ring c₁ is non empty left_add-cancelable right_add-cancelable right_complementable strict Abelian add-associative right_zeroed unital commutative right-distributive left-distributive right_unital well-unital distributive left_unital V174() V175() V176() V177() doubleLoopStr
power (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁),NAT) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)))
the carrier of (Polynom-Ring c₁) is non empty set
K28( the carrier of (Polynom-Ring c₁),NAT) is INT -valued RAT -valued V24() complex-valued ext-real-valued real-valued natural-valued set
K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁)) is V24() set
K27(K28(K28( the carrier of (Polynom-Ring c₁),NAT), the carrier of (Polynom-Ring c₁))) is V24() set
(power (Polynom-Ring c₁)) . (np,3) is set
np *' np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
(np *' np) *' np is Relation-like NAT -defined the carrier of c₁ -valued Function-like non empty total quasi_total finite-Support Element of K27(K28(NAT, the carrier of c₁))
z0 is Element of the carrier of (Polynom-Ring c₁)
z0 * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) is Relation-like K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)) -defined the carrier of (Polynom-Ring c₁) -valued Function-like total quasi_total Element of K27(K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁)))
K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)) is set
K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁)) is set
K27(K28(K28( the carrier of (Polynom-Ring c₁), the carrier of (Polynom-Ring c₁)), the carrier of (Polynom-Ring c₁))) is set
the multF of (Polynom-Ring c₁) . (z0,z0) is Element of the carrier of (Polynom-Ring c₁)
2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power (Polynom-Ring c₁)) . (z0,(2 + 1)) is Element of the carrier of (Polynom-Ring c₁)
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power (Polynom-Ring c₁)) . (z0,(1 + 1)) is Element of the carrier of (Polynom-Ring c₁)
((power (Polynom-Ring c₁)) . (z0,(1 + 1))) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (((power (Polynom-Ring c₁)) . (z0,(1 + 1))),z0) is Element of the carrier of (Polynom-Ring c₁)
0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V24() V29() complex real ext-real positive non negative V54() V55() V56() V57() V58() V59() V60() V61() Element of NAT
(power (Polynom-Ring c₁)) . (z0,(0 + 1)) is Element of the carrier of (Polynom-Ring c₁)
((power (Polynom-Ring c₁)) . (z0,(0 + 1))) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (((power (Polynom-Ring c₁)) . (z0,(0 + 1))),z0) is Element of the carrier of (Polynom-Ring c₁)
(((power (Polynom-Ring c₁)) . (z0,(0 + 1))) * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . ((((power (Polynom-Ring c₁)) . (z0,(0 + 1))) * z0),z0) is Element of the carrier of (Polynom-Ring c₁)
(power (Polynom-Ring c₁)) . (z0,0) is Element of the carrier of (Polynom-Ring c₁)
((power (Polynom-Ring c₁)) . (z0,0)) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (((power (Polynom-Ring c₁)) . (z0,0)),z0) is Element of the carrier of (Polynom-Ring c₁)
(((power (Polynom-Ring c₁)) . (z0,0)) * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . ((((power (Polynom-Ring c₁)) . (z0,0)) * z0),z0) is Element of the carrier of (Polynom-Ring c₁)
((((power (Polynom-Ring c₁)) . (z0,0)) * z0) * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (((((power (Polynom-Ring c₁)) . (z0,0)) * z0) * z0),z0) is Element of the carrier of (Polynom-Ring c₁)
1_ (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
1. (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
the OneF of (Polynom-Ring c₁) is Element of the carrier of (Polynom-Ring c₁)
(1_ (Polynom-Ring c₁)) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . ((1_ (Polynom-Ring c₁)),z0) is Element of the carrier of (Polynom-Ring c₁)
((1_ (Polynom-Ring c₁)) * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . (((1_ (Polynom-Ring c₁)) * z0),z0) is Element of the carrier of (Polynom-Ring c₁)
(((1_ (Polynom-Ring c₁)) * z0) * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (Polynom-Ring c₁) . ((((1_ (Polynom-Ring c₁)) * z0) * z0),z0) is Element of the carrier of (Polynom-Ring c₁)
(z0 * z0) * z0 is Element of the carrier of (Polynom-Ring c₁)
the multF of (