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

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

(c

- c

(c

((c

- np is complex real ext-real non positive V54() set

((c

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

(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

c

(c

np is complex real ext-real set

c

min (c

max (c

(min (c

(max (c

(min (c

np is complex real ext-real set

c

max (c

min (c

2 * (max (c

(min (c

(2 * (max (c

(min (c

np * 2 is complex real ext-real Element of REAL

(min (c

(max (c

(min (c

((min (c

((min (c

2 " is non empty complex real ext-real positive non negative set

((min (c

(max (c

(min (c

((max (c

(min (c

((min (c

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 set

c

(c

c

c

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

np is complex real ext-real Element of REAL

c

z0 is complex real ext-real set

z0 * c

c

dom c

Sum c

K294(REAL,c

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

dom (c

Sum (c

K294(REAL,(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

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

Sum (c

K294(REAL,(c

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

Sum (c

K294(REAL,(c

len c

c

<*(c

(c

(Sum (c

c

len c

len 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

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

(len c

len (c

(c

(c

c

(c

(c

c

Seg ((len c

Seg (len c

{((len c

(Seg (len c

(dom c

c

Sum (c

K294(REAL,(c

(Sum c

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

0 + ((c

(Sum c

dom (<*> REAL) is epsilon-transitive epsilon-connected ordinal V56() V57() V58() V59() V60() V61() Element of K27(NAT)

c

(<*> REAL) . c

c

np is complex real ext-real Element of REAL

[**c

<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

- [**c

- c

- np is complex real ext-real Element of REAL

[**(- c

(- np) * <i> is complex set

(- c

- (c

c

np is complex real ext-real Element of REAL

[**c

<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

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

- [**z0,k**] is complex Element of the carrier of F_Complex

[**c

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

K593([**c

c

- z0 is complex real ext-real set

c

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

(np - k) * <i> is complex set

(c

- 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

the addF of F_Complex . ([**c

K593([**c

c

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

(power F_Complex) . (c

|.((power F_Complex) . (c

|.c

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

|.((power F_Complex) . (c

|.c

((power F_Complex) . (c

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

K595(((power F_Complex) . (c

|.(((power F_Complex) . (c

(|.c

|.c

(|.c

(power F_Complex) . (c

|.((power F_Complex) . (c

|.c

c

len c

dom 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

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

|.(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

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

|.(c

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

<*c

(<*c

|.c

<*|.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

Seg (0 + 1) is non empty V24() V31(0 + 1) V56() V57() V58() V59() V60() V61() Element of K27(NAT)

dom <*c

len (<*c

len <*c

dom (<*c

np is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set

(<*c

(<*c

<*c

|.(<*c

<*|.c

len <*|.c

c

np is complex Element of the carrier of F_Complex

<*c

K250(2, the carrier of F_Complex) is M12( the carrier of F_Complex)

(<*c

|.c

|.np.| is complex real ext-real Element of REAL

<*|.c

K250(2,REAL) is M12( REAL )

len (<*c

len <*c

dom (<*c

z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set

dom <*c

(<*c

(<*c

<*c

|.(<*c

(<*c

<*|.c

dom <*c

(<*c

(<*c

<*c

|.(<*c

(<*c

<*|.c

len <*|.c

c

np is complex Element of the carrier of F_Complex

z0 is complex Element of the carrier of F_Complex

<*c

(<*c

|.c

|.np.| is complex real ext-real Element of REAL

|.z0.| is complex real ext-real Element of REAL

<*|.c

len (<*c

len <*c

dom (<*c

k is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set

dom <*c

(<*c

(<*c

<*c

|.(<*c

(<*c

<*|.c

dom <*c

(<*c

(<*c

<*c

|.(<*c

(<*c

<*|.c

dom <*c

(<*c

(<*c

<*c

|.(<*c

(<*c

<*|.c

len <*|.c

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

((c

(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

dom ((c

len ((c

Seg (len ((c

len (c

len c

z0 is epsilon-transitive epsilon-connected ordinal natural V24() V29() complex real ext-real non negative V54() set

len (c

dom (c

dom c

(c

(c

c

c

dom (c

((c

((c

|.((c

(c

(c

((c

dom c

0 + (len c

z0 - (len c

- (len c

z0 + (- (len c

(len c

z0 -' (len c

(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) + (len c

1 + (len c

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

(c

np . (z0 -' (len c

np /. (z0 -' (len c

((c

((c

|.((c

(np) /. (z0 -' (len c

(np) . (z0 -' (len c

((c

dom 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

(len (c

len ((c

c

(c

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

((c

|.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*> ^ c

((<*np*> ^ c

<*|.np.|*> ^ (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

(<*np*>) ^ (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

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

the carrier of c

K28(NAT, the carrier of c

K27(K28(NAT, the carrier of c

Polynom-Ring c

power (Polynom-Ring c

the carrier of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

np is Relation-like NAT -defined 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

k is Element of the carrier of (Polynom-Ring c

(power (Polynom-Ring c

c

the carrier of c

K28(NAT, the carrier of c

K27(K28(NAT, the carrier of c

np is Relation-like NAT -defined 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

Polynom-Ring c

power (Polynom-Ring c

the carrier of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

(power (Polynom-Ring c

k is Element of the carrier of (Polynom-Ring c

(power (Polynom-Ring c

c

the carrier of c

K28(NAT, the carrier of c

K27(K28(NAT, the carrier of c

1_. c

0_. c

0. c

the ZeroF of c

NAT --> (0. c

1. c

the OneF of c

(0_. c

np is Relation-like NAT -defined the carrier of c

(c

Polynom-Ring c

power (Polynom-Ring c

the carrier of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

(power (Polynom-Ring c

z0 is Element of the carrier of (Polynom-Ring c

(power (Polynom-Ring c

1_ (Polynom-Ring c

1. (Polynom-Ring c

the OneF of (Polynom-Ring c

c

the carrier of c

K28(NAT, the carrier of c

K27(K28(NAT, the carrier of c

np is Relation-like NAT -defined the carrier of c

(c

Polynom-Ring c

power (Polynom-Ring c

the carrier of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

(power (Polynom-Ring c

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

(power (Polynom-Ring c

((power (Polynom-Ring c

the multF of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

the multF of (Polynom-Ring c

1_ (Polynom-Ring c

1. (Polynom-Ring c

the OneF of (Polynom-Ring c

(1_ (Polynom-Ring c

the multF of (Polynom-Ring c

c

the carrier of c

K28(NAT, the carrier of c

K27(K28(NAT, the carrier of c

np is Relation-like NAT -defined the carrier of c

(c

Polynom-Ring c

power (Polynom-Ring c

the carrier of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

(power (Polynom-Ring c

np *' np is Relation-like NAT -defined 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

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

((power (Polynom-Ring c

the multF of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

the multF of (Polynom-Ring c

(power (Polynom-Ring c

((power (Polynom-Ring c

the multF of (Polynom-Ring c

(((power (Polynom-Ring c

the multF of (Polynom-Ring c

1_ (Polynom-Ring c

1. (Polynom-Ring c

the OneF of (Polynom-Ring c

(1_ (Polynom-Ring c

the multF of (Polynom-Ring c

((1_ (Polynom-Ring c

the multF of (Polynom-Ring c

z0 * z0 is Element of the carrier of (Polynom-Ring c

the multF of (Polynom-Ring c

c

the carrier of c

K28(NAT, the carrier of c

K27(K28(NAT, the carrier of c

np is Relation-like NAT -defined the carrier of c

(c

Polynom-Ring c

power (Polynom-Ring c

the carrier of (Polynom-Ring c

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

(power (Polynom-Ring c

np *' np is Relation-like NAT -defined the carrier of c

(np *' np) *' np is Relation-like NAT -defined 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

K28( the carrier of (Polynom-Ring c

K28(K28( the carrier of (Polynom-Ring c

K27(K28(K28( the carrier of (Polynom-Ring c

the multF 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

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

((power (Polynom-Ring c

the multF 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

((power (Polynom-Ring c

the multF of (Polynom-Ring c

(((power (Polynom-Ring c

the multF of (Polynom-Ring c

(power (Polynom-Ring c

((power (Polynom-Ring c

the multF of (Polynom-Ring c

(((power (Polynom-Ring c

the multF of (Polynom-Ring c

((((power (Polynom-Ring c

the multF of (Polynom-Ring c

1_ (Polynom-Ring c

1. (Polynom-Ring c

the OneF of (Polynom-Ring c

(1_ (Polynom-Ring c

the multF of (Polynom-Ring c

((1_ (Polynom-Ring c

the multF of (Polynom-Ring c

(((1_ (Polynom-Ring c

the multF of (Polynom-Ring c

(z0 * z0) * z0 is Element of the carrier of (Polynom-Ring c

the multF of (