:: HURWITZ semantic presentation

REAL is set

NAT is non empty V24() V25() V26() V40() V45() V46() Element of K19(REAL)

K19(REAL) is set

F_Complex is non empty non degenerated V72() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like V150() V151() V152() V153() algebraic-closed doubleLoopStr

the carrier of F_Complex is non empty V12() set

COMPLEX is set

NAT is non empty V24() V25() V26() V40() V45() V46() set

K19(NAT) is V40() set

K19(NAT) is V40() set

K141(NAT) is V39() set

RAT is set

INT is set

K20(COMPLEX,COMPLEX) is set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is V40() set

K20(K20(NAT,NAT),NAT) is V40() set

K19(K20(K20(NAT,NAT),NAT)) is V40() set

K280() is set

1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

{} is functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-membered integer set

2 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

K20(NAT,REAL) is set

K19(K20(NAT,REAL)) is set

K271(1,NAT) is M8( NAT )

3 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

0 is functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-membered integer Element of NAT

Seg 1 is non empty V12() V40() V47(1) Element of K19(NAT)

{ b

{1} is non empty V12() V47(1) set

Seg 2 is non empty V40() V47(2) Element of K19(NAT)

{ b

{1,2} is non empty set

K204() is Relation-like K20(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))

K206() is Relation-like K20(COMPLEX,COMPLEX) -defined COMPLEX -valued Function-like V18(K20(COMPLEX,COMPLEX), COMPLEX ) Element of K19(K20(K20(COMPLEX,COMPLEX),COMPLEX))

1r is complex Element of COMPLEX

0c is functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-membered integer Element of COMPLEX

0. F_Complex is complex zero 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

(0. F_Complex) *' is complex Element of the carrier of F_Complex

Re (0. F_Complex) is complex V32() ext-real Element of REAL

Im (0. F_Complex) is complex V32() ext-real Element of REAL

<i> is complex Element of COMPLEX

(Im (0. F_Complex)) * <i> is complex set

(Re (0. F_Complex)) - ((Im (0. F_Complex)) * <i>) is complex set

(1. F_Complex) *' is complex Element of the carrier of F_Complex

Re (1. F_Complex) is complex V32() ext-real Element of REAL

Im (1. F_Complex) is complex V32() ext-real Element of REAL

(Im (1. F_Complex)) * <i> is complex set

(Re (1. F_Complex)) - ((Im (1. F_Complex)) * <i>) is complex set

K20(NAT, the carrier of F_Complex) is V40() set

K19(K20(NAT, the carrier of F_Complex)) is V40() set

Re 0 is complex V32() ext-real Element of REAL

Im 0 is complex V32() ext-real Element of REAL

Re 1r is complex V32() ext-real Element of REAL

Im 1r is complex V32() ext-real Element of REAL

0 *' is complex Element of COMPLEX

(Im 0) * <i> is complex set

(Re 0) - ((Im 0) * <i>) is complex set

f is non empty left_add-cancelable right_add-cancelable right_complementable add-associative right_zeroed V150() V151() V152() V153() addLoopStr

the carrier of f is non empty set

rho is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom rho is Element of K19(NAT)

ef is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set

dom ef is Element of K19(NAT)

len ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer set

Seg ef1 is V40() V47(ef1) Element of K19(NAT)

{ b

rho | (Seg ef1) is Relation-like NAT -defined the carrier of f -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of f))

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

ef1 + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

rho /. (ef1 + 1) is Element of the carrier of f

<*(rho /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of f

[1,(rho /. (ef1 + 1))] is set

{[1,(rho /. (ef1 + 1))]} is non empty V12() V47(1) set

ef ^ <*(rho /. (ef1 + 1))*> is Relation-like NAT -defined Function-like non empty V40() FinSequence-like FinSubsequence-like set

t is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

b9 is set

rng t is set

dom t is Element of K19(NAT)

zz is set

t . zz is set

a1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

rho . zz is set

rho /. zz is Element of the carrier of f

b9 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

b9 ^ <*(rho /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

dom (b9 ^ <*(rho /. (ef1 + 1))*>) is Element of K19(NAT)

len b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

len <*(rho /. (ef1 + 1))*> is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(len b9) + (len <*(rho /. (ef1 + 1))*>) is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

Seg ((len b9) + (len <*(rho /. (ef1 + 1))*>)) is non empty V40() V47((len b9) + (len <*(rho /. (ef1 + 1))*>)) Element of K19(NAT)

{ b

Seg (ef1 + 1) is non empty V40() V47(ef1 + 1) Element of K19(NAT)

{ b

zz is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer set

dom b9 is Element of K19(NAT)

rho . zz is set

b9 . zz is set

(b9 ^ <*(rho /. (ef1 + 1))*>) . zz is set

dom b9 is Element of K19(NAT)

Seg (len rho) is V40() V47( len rho) Element of K19(NAT)

{ b

dom <*(rho /. (ef1 + 1))*> is non empty V12() V47(1) Element of K19(NAT)

(b9 ^ <*(rho /. (ef1 + 1))*>) . zz is set

<*(rho /. (ef1 + 1))*> . 1 is set

rho . zz is set

dom b9 is Element of K19(NAT)

f is non empty left_add-cancelable right_add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty set

0. f is zero Element of the carrier of f

rho is Element of the carrier of f

rho " is Element of the carrier of f

- (rho ") is Element of the carrier of f

- rho is Element of the carrier of f

(- rho) " is Element of the carrier of f

- (- rho) is Element of the carrier of f

(- rho) * (- (rho ")) is Element of the carrier of f

(- rho) * (rho ") is Element of the carrier of f

- ((- rho) * (rho ")) is Element of the carrier of f

rho * (rho ") is Element of the carrier of f

- (rho * (rho ")) is Element of the carrier of f

- (- (rho * (rho "))) is Element of the carrier of f

1_ f is Element of the carrier of f

1. f is Element of the carrier of f

- (1_ f) is Element of the carrier of f

- (- (1_ f)) is Element of the carrier of f

f is non empty non degenerated V72() left_add-cancelable right_add-cancelable right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed domRing-like V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty V12() set

power f is Relation-like K20( the carrier of f,NAT) -defined the carrier of f -valued Function-like total V18(K20( the carrier of f,NAT), the carrier of f) Element of K19(K20(K20( the carrier of f,NAT), the carrier of f))

K20( the carrier of f,NAT) is V40() set

K20(K20( the carrier of f,NAT), the carrier of f) is V40() set

K19(K20(K20( the carrier of f,NAT), the carrier of f)) is V40() set

1_ f is Element of the carrier of f

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

- (1_ f) is Element of the carrier of f

0. f is zero Element of the carrier of f

rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),rho) is Element of the carrier of f

(1_ f) * (1_ f) is Element of the carrier of f

(- (1_ f)) * (- (1_ f)) is Element of the carrier of f

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),(ef + 1)) is Element of the carrier of f

(power f) . ((- (1_ f)),ef) is Element of the carrier of f

((power f) . ((- (1_ f)),ef)) * (- (1_ f)) is Element of the carrier of f

(power f) . ((- (1_ f)),ef) is set

(power f) . ((- (1_ f)),(ef + 1)) is set

(power f) . ((- (1_ f)),0) is set

f is non empty unital associative right_unital well-unital left_unital multLoopStr

the carrier of f is non empty set

power f is Relation-like K20( the carrier of f,NAT) -defined the carrier of f -valued Function-like total V18(K20( the carrier of f,NAT), the carrier of f) Element of K19(K20(K20( the carrier of f,NAT), the carrier of f))

K20( the carrier of f,NAT) is V40() set

K20(K20( the carrier of f,NAT), the carrier of f) is V40() set

K19(K20(K20( the carrier of f,NAT), the carrier of f)) is V40() set

rho is Element of the carrier of f

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,ef) is Element of the carrier of f

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,ef1) is Element of the carrier of f

((power f) . (rho,ef)) * ((power f) . (rho,ef1)) is Element of the carrier of f

ef + ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,(ef + ef1)) is Element of the carrier of f

t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . (rho,(t + 1)) is Element of the carrier of f

((power f) . (rho,ef)) * ((power f) . (rho,(t + 1))) is Element of the carrier of f

(power f) . (rho,t) is Element of the carrier of f

((power f) . (rho,t)) * rho is Element of the carrier of f

((power f) . (rho,ef)) * (((power f) . (rho,t)) * rho) is Element of the carrier of f

((power f) . (rho,ef)) * ((power f) . (rho,t)) is Element of the carrier of f

(((power f) . (rho,ef)) * ((power f) . (rho,t))) * rho is Element of the carrier of f

ef + t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(ef + t) + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . (rho,((ef + t) + 1)) is Element of the carrier of f

ef + (t + 1) is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . (rho,(ef + (t + 1))) is Element of the carrier of f

b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,b9) is Element of the carrier of f

((power f) . (rho,ef)) * ((power f) . (rho,b9)) is Element of the carrier of f

ef + b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,(ef + b9)) is Element of the carrier of f

1_ f is Element of the carrier of f

1. f is Element of the carrier of f

(power f) . (rho,0) is Element of the carrier of f

((power f) . (rho,ef)) * ((power f) . (rho,0)) is Element of the carrier of f

((power f) . (rho,ef)) * (1. f) is Element of the carrier of f

ef + 0 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,(ef + 0)) is Element of the carrier of f

t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,t) is Element of the carrier of f

((power f) . (rho,ef)) * ((power f) . (rho,t)) is Element of the carrier of f

ef + t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . (rho,(ef + t)) is Element of the carrier of f

Im (1_ F_Complex) is complex V32() ext-real Element of REAL

- (1_ F_Complex) is complex Element of the carrier of F_Complex

Im (- (1_ F_Complex)) is complex V32() ext-real Element of REAL

- 1r is complex Element of COMPLEX

- 0 is functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-membered integer set

f is non empty left_add-cancelable right_add-cancelable right_complementable unital right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty set

power f is Relation-like K20( the carrier of f,NAT) -defined the carrier of f -valued Function-like total V18(K20( the carrier of f,NAT), the carrier of f) Element of K19(K20(K20( the carrier of f,NAT), the carrier of f))

K20( the carrier of f,NAT) is V40() set

K20(K20( the carrier of f,NAT), the carrier of f) is V40() set

K19(K20(K20( the carrier of f,NAT), the carrier of f)) is V40() set

1_ f is Element of the carrier of f

1. f is Element of the carrier of f

- (1_ f) is Element of the carrier of f

rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

2 * rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),(2 * rho)) is Element of the carrier of f

(2 * rho) + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),((2 * rho) + 1)) is Element of the carrier of f

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

2 * ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),(2 * ef)) is Element of the carrier of f

(2 * ef) + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),((2 * ef) + 1)) is Element of the carrier of f

ef + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

2 * (ef + 1) is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),(2 * (ef + 1))) is Element of the carrier of f

((2 * ef) + 1) + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),(((2 * ef) + 1) + 1)) is Element of the carrier of f

((power f) . ((- (1_ f)),((2 * ef) + 1))) * (- (1_ f)) is Element of the carrier of f

(1_ f) * (- (1_ f)) is Element of the carrier of f

- ((1_ f) * (- (1_ f))) is Element of the carrier of f

- (- (1_ f)) is Element of the carrier of f

(2 * (ef + 1)) + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),((2 * (ef + 1)) + 1)) is Element of the carrier of f

((power f) . ((- (1_ f)),(2 * (ef + 1)))) * (- (1_ f)) is Element of the carrier of f

2 * 0 is functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-membered integer Element of NAT

(2 * 0) + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power f) . ((- (1_ f)),((2 * 0) + 1)) is Element of the carrier of f

(power f) . ((- (1_ f)),0) is Element of the carrier of f

((power f) . ((- (1_ f)),0)) * (- (1_ f)) is Element of the carrier of f

(power f) . ((- (1_ f)),(2 * 0)) is Element of the carrier of f

power F_Complex is Relation-like K20( the carrier of F_Complex,NAT) -defined the carrier of F_Complex -valued Function-like total V18(K20( the carrier of F_Complex,NAT), the carrier of F_Complex) Element of K19(K20(K20( the carrier of F_Complex,NAT), the carrier of F_Complex))

K20( the carrier of F_Complex,NAT) is V40() set

K20(K20( the carrier of F_Complex,NAT), the carrier of F_Complex) is V40() set

K19(K20(K20( the carrier of F_Complex,NAT), the carrier of F_Complex)) is V40() set

f is complex Element of the carrier of F_Complex

f *' is complex Element of the carrier of F_Complex

Re f is complex V32() ext-real Element of REAL

Im f is complex V32() ext-real Element of REAL

(Im f) * <i> is complex set

(Re f) - ((Im f) * <i>) is complex set

rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power F_Complex) . (f,rho) is complex Element of the carrier of F_Complex

((power F_Complex) . (f,rho)) *' is complex Element of the carrier of F_Complex

Re ((power F_Complex) . (f,rho)) is complex V32() ext-real Element of REAL

Im ((power F_Complex) . (f,rho)) is complex V32() ext-real Element of REAL

(Im ((power F_Complex) . (f,rho))) * <i> is complex set

(Re ((power F_Complex) . (f,rho))) - ((Im ((power F_Complex) . (f,rho))) * <i>) is complex set

(power F_Complex) . ((f *'),rho) is complex Element of the carrier of F_Complex

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

(power F_Complex) . (f,(ef + 1)) is complex Element of the carrier of F_Complex

((power F_Complex) . (f,(ef + 1))) *' is complex Element of the carrier of F_Complex

Re ((power F_Complex) . (f,(ef + 1))) is complex V32() ext-real Element of REAL

Im ((power F_Complex) . (f,(ef + 1))) is complex V32() ext-real Element of REAL

(Im ((power F_Complex) . (f,(ef + 1)))) * <i> is complex set

(Re ((power F_Complex) . (f,(ef + 1)))) - ((Im ((power F_Complex) . (f,(ef + 1)))) * <i>) is complex set

(power F_Complex) . (f,ef) is complex Element of the carrier of F_Complex

((power F_Complex) . (f,ef)) * f is complex Element of the carrier of F_Complex

K182(((power F_Complex) . (f,ef)),f) is complex Element of COMPLEX

(((power F_Complex) . (f,ef)) * f) *' is complex Element of the carrier of F_Complex

Re (((power F_Complex) . (f,ef)) * f) is complex V32() ext-real Element of REAL

Im (((power F_Complex) . (f,ef)) * f) is complex V32() ext-real Element of REAL

(Im (((power F_Complex) . (f,ef)) * f)) * <i> is complex set

(Re (((power F_Complex) . (f,ef)) * f)) - ((Im (((power F_Complex) . (f,ef)) * f)) * <i>) is complex set

(power F_Complex) . ((f *'),ef) is complex Element of the carrier of F_Complex

((power F_Complex) . ((f *'),ef)) * (f *') is complex Element of the carrier of F_Complex

K182(((power F_Complex) . ((f *'),ef)),(f *')) is complex Element of COMPLEX

(power F_Complex) . ((f *'),(ef + 1)) is complex Element of the carrier of F_Complex

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power F_Complex) . (f,ef1) is complex Element of the carrier of F_Complex

((power F_Complex) . (f,ef1)) *' is complex Element of the carrier of F_Complex

Re ((power F_Complex) . (f,ef1)) is complex V32() ext-real Element of REAL

Im ((power F_Complex) . (f,ef1)) is complex V32() ext-real Element of REAL

(Im ((power F_Complex) . (f,ef1))) * <i> is complex set

(Re ((power F_Complex) . (f,ef1))) - ((Im ((power F_Complex) . (f,ef1))) * <i>) is complex set

(power F_Complex) . ((f *'),ef1) is complex Element of the carrier of F_Complex

(power F_Complex) . (f,0) is complex Element of the carrier of F_Complex

((power F_Complex) . (f,0)) *' is complex Element of the carrier of F_Complex

Re ((power F_Complex) . (f,0)) is complex V32() ext-real Element of REAL

Im ((power F_Complex) . (f,0)) is complex V32() ext-real Element of REAL

(Im ((power F_Complex) . (f,0))) * <i> is complex set

(Re ((power F_Complex) . (f,0))) - ((Im ((power F_Complex) . (f,0))) * <i>) is complex set

(1_ F_Complex) *' is complex Element of the carrier of F_Complex

Re (1_ F_Complex) is complex V32() ext-real Element of REAL

(Im (1_ F_Complex)) * <i> is complex set

(Re (1_ F_Complex)) - ((Im (1_ F_Complex)) * <i>) is complex set

(power F_Complex) . ((f *'),0) is complex Element of the carrier of F_Complex

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

(power F_Complex) . (f,ef) is complex Element of the carrier of F_Complex

((power F_Complex) . (f,ef)) *' is complex Element of the carrier of F_Complex

Re ((power F_Complex) . (f,ef)) is complex V32() ext-real Element of REAL

Im ((power F_Complex) . (f,ef)) is complex V32() ext-real Element of REAL

(Im ((power F_Complex) . (f,ef))) * <i> is complex set

(Re ((power F_Complex) . (f,ef))) - ((Im ((power F_Complex) . (f,ef))) * <i>) is complex set

(power F_Complex) . ((f *'),ef) is complex Element of the carrier of F_Complex

rho is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

f is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len f is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom rho is Element of K19(NAT)

Sum rho is complex Element of the carrier of F_Complex

Sum f is complex Element of the carrier of F_Complex

(Sum f) *' is complex Element of the carrier of F_Complex

Re (Sum f) is complex V32() ext-real Element of REAL

Im (Sum f) is complex V32() ext-real Element of REAL

(Im (Sum f)) * <i> is complex set

(Re (Sum f)) - ((Im (Sum f)) * <i>) is complex set

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

dom t is Element of K19(NAT)

Seg ef is V40() V47(ef) Element of K19(NAT)

{ b

t | (Seg ef) is Relation-like NAT -defined the carrier of F_Complex -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of F_Complex))

zz is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set

a1 is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

t /. (ef + 1) is complex Element of the carrier of F_Complex

<*(t /. (ef + 1))*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

[1,(t /. (ef + 1))] is set

{[1,(t /. (ef + 1))]} is non empty V12() V47(1) set

a1 ^ <*(t /. (ef + 1))*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

ef1 | (Seg ef) is Relation-like NAT -defined the carrier of F_Complex -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of F_Complex))

a19 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set

b19 is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len b19 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

len a1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom a1 is Element of K19(NAT)

Seg (len b19) is V40() V47( len b19) Element of K19(NAT)

{ b

dom b19 is Element of K19(NAT)

ef1 /. (ef + 1) is complex Element of the carrier of F_Complex

<*(ef1 /. (ef + 1))*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

[1,(ef1 /. (ef + 1))] is set

{[1,(ef1 /. (ef + 1))]} is non empty V12() V47(1) set

b19 ^ <*(ef1 /. (ef + 1))*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

Seg (len ef1) is V40() V47( len ef1) Element of K19(NAT)

{ b

dom ef1 is Element of K19(NAT)

z is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 /. z is complex Element of the carrier of F_Complex

ef1 . z is set

b19 . z is set

b19 /. z is complex Element of the carrier of F_Complex

a1 /. z is complex Element of the carrier of F_Complex

a1 . z is set

t . z is set

t /. z is complex Element of the carrier of F_Complex

(b19 /. z) *' is complex Element of the carrier of F_Complex

Re (b19 /. z) is complex V32() ext-real Element of REAL

Im (b19 /. z) is complex V32() ext-real Element of REAL

(Im (b19 /. z)) * <i> is complex set

(Re (b19 /. z)) - ((Im (b19 /. z)) * <i>) is complex set

Sum ef1 is complex Element of the carrier of F_Complex

(Sum ef1) *' is complex Element of the carrier of F_Complex

Re (Sum ef1) is complex V32() ext-real Element of REAL

Im (Sum ef1) is complex V32() ext-real Element of REAL

(Im (Sum ef1)) * <i> is complex set

(Re (Sum ef1)) - ((Im (Sum ef1)) * <i>) is complex set

Sum b19 is complex Element of the carrier of F_Complex

Sum <*(ef1 /. (ef + 1))*> is complex Element of the carrier of F_Complex

(Sum b19) + (Sum <*(ef1 /. (ef + 1))*>) is complex Element of the carrier of F_Complex

K180((Sum b19),(Sum <*(ef1 /. (ef + 1))*>)) is complex Element of COMPLEX

((Sum b19) + (Sum <*(ef1 /. (ef + 1))*>)) *' is complex Element of the carrier of F_Complex

Re ((Sum b19) + (Sum <*(ef1 /. (ef + 1))*>)) is complex V32() ext-real Element of REAL

Im ((Sum b19) + (Sum <*(ef1 /. (ef + 1))*>)) is complex V32() ext-real Element of REAL

(Im ((Sum b19) + (Sum <*(ef1 /. (ef + 1))*>))) * <i> is complex set

(Re ((Sum b19) + (Sum <*(ef1 /. (ef + 1))*>))) - ((Im ((Sum b19) + (Sum <*(ef1 /. (ef + 1))*>))) * <i>) is complex set

(Sum b19) *' is complex Element of the carrier of F_Complex

Re (Sum b19) is complex V32() ext-real Element of REAL

Im (Sum b19) is complex V32() ext-real Element of REAL

(Im (Sum b19)) * <i> is complex set

(Re (Sum b19)) - ((Im (Sum b19)) * <i>) is complex set

(Sum <*(ef1 /. (ef + 1))*>) *' is complex Element of the carrier of F_Complex

Re (Sum <*(ef1 /. (ef + 1))*>) is complex V32() ext-real Element of REAL

Im (Sum <*(ef1 /. (ef + 1))*>) is complex V32() ext-real Element of REAL

(Im (Sum <*(ef1 /. (ef + 1))*>)) * <i> is complex set

(Re (Sum <*(ef1 /. (ef + 1))*>)) - ((Im (Sum <*(ef1 /. (ef + 1))*>)) * <i>) is complex set

((Sum b19) *') + ((Sum <*(ef1 /. (ef + 1))*>) *') is complex Element of the carrier of F_Complex

K180(((Sum b19) *'),((Sum <*(ef1 /. (ef + 1))*>) *')) is complex Element of COMPLEX

Sum a1 is complex Element of the carrier of F_Complex

(Sum a1) + ((Sum <*(ef1 /. (ef + 1))*>) *') is complex Element of the carrier of F_Complex

K180((Sum a1),((Sum <*(ef1 /. (ef + 1))*>) *')) is complex Element of COMPLEX

(ef1 /. (ef + 1)) *' is complex Element of the carrier of F_Complex

Re (ef1 /. (ef + 1)) is complex V32() ext-real Element of REAL

Im (ef1 /. (ef + 1)) is complex V32() ext-real Element of REAL

(Im (ef1 /. (ef + 1))) * <i> is complex set

(Re (ef1 /. (ef + 1))) - ((Im (ef1 /. (ef + 1))) * <i>) is complex set

(Sum a1) + ((ef1 /. (ef + 1)) *') is complex Element of the carrier of F_Complex

K180((Sum a1),((ef1 /. (ef + 1)) *')) is complex Element of COMPLEX

(Sum a1) + (t /. (ef + 1)) is complex Element of the carrier of F_Complex

K180((Sum a1),(t /. (ef + 1))) is complex Element of COMPLEX

Sum <*(t /. (ef + 1))*> is complex Element of the carrier of F_Complex

(Sum a1) + (Sum <*(t /. (ef + 1))*>) is complex Element of the carrier of F_Complex

K180((Sum a1),(Sum <*(t /. (ef + 1))*>)) is complex Element of COMPLEX

Sum t is complex Element of the carrier of F_Complex

t is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom t is Element of K19(NAT)

Sum t is complex Element of the carrier of F_Complex

Sum ef1 is complex Element of the carrier of F_Complex

(Sum ef1) *' is complex Element of the carrier of F_Complex

Re (Sum ef1) is complex V32() ext-real Element of REAL

Im (Sum ef1) is complex V32() ext-real Element of REAL

(Im (Sum ef1)) * <i> is complex set

(Re (Sum ef1)) - ((Im (Sum ef1)) * <i>) is complex set

ef is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom ef1 is Element of K19(NAT)

<*> the carrier of F_Complex is Relation-like NAT -defined the carrier of F_Complex -valued Function-like functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-like FinSubsequence-like FinSequence-membered integer Function-yielding V54() FinSequence of the carrier of F_Complex

Sum ef is complex Element of the carrier of F_Complex

Sum ef1 is complex Element of the carrier of F_Complex

(Sum ef) *' is complex Element of the carrier of F_Complex

Re (Sum ef) is complex V32() ext-real Element of REAL

Im (Sum ef) is complex V32() ext-real Element of REAL

(Im (Sum ef)) * <i> is complex set

(Re (Sum ef)) - ((Im (Sum ef)) * <i>) is complex set

ef1 is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Complex

len ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom ef1 is Element of K19(NAT)

Sum ef1 is complex Element of the carrier of F_Complex

Sum ef is complex Element of the carrier of F_Complex

(Sum ef) *' is complex Element of the carrier of F_Complex

Re (Sum ef) is complex V32() ext-real Element of REAL

Im (Sum ef) is complex V32() ext-real Element of REAL

(Im (Sum ef)) * <i> is complex set

(Re (Sum ef)) - ((Im (Sum ef)) * <i>) is complex set

f is non empty left_add-cancelable right_add-cancelable right_complementable Abelian add-associative right_zeroed V150() V151() V152() V153() addLoopStr

the carrier of f is non empty set

rho is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom rho is Element of K19(NAT)

Sum rho is Element of the carrier of f

Sum ef is Element of the carrier of f

- (Sum ef) is Element of the carrier of f

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

b9 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom t is Element of K19(NAT)

Seg ef1 is V40() V47(ef1) Element of K19(NAT)

{ b

t | (Seg ef1) is Relation-like NAT -defined the carrier of f -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of f))

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

b9 | (Seg ef1) is Relation-like NAT -defined the carrier of f -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of f))

b1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set

a19 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set

b19 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len b19 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

z is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len z is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom b19 is Element of K19(NAT)

Seg (len z) is V40() V47( len z) Element of K19(NAT)

{ b

dom z is Element of K19(NAT)

t /. (ef1 + 1) is Element of the carrier of f

<*(t /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of f

[1,(t /. (ef1 + 1))] is set

{[1,(t /. (ef1 + 1))]} is non empty V12() V47(1) set

b19 ^ <*(t /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

b9 /. (ef1 + 1) is Element of the carrier of f

<*(b9 /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of f

[1,(b9 /. (ef1 + 1))] is set

{[1,(b9 /. (ef1 + 1))]} is non empty V12() V47(1) set

z ^ <*(b9 /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

g1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom b9 is Element of K19(NAT)

b9 /. g1 is Element of the carrier of f

b9 . g1 is set

z . g1 is set

z /. g1 is Element of the carrier of f

b19 /. g1 is Element of the carrier of f

b19 . g1 is set

t . g1 is set

t /. g1 is Element of the carrier of f

- (z /. g1) is Element of the carrier of f

Sum t is Element of the carrier of f

Sum b19 is Element of the carrier of f

Sum <*(t /. (ef1 + 1))*> is Element of the carrier of f

(Sum b19) + (Sum <*(t /. (ef1 + 1))*>) is Element of the carrier of f

Sum z is Element of the carrier of f

- (Sum z) is Element of the carrier of f

(- (Sum z)) + (Sum <*(t /. (ef1 + 1))*>) is Element of the carrier of f

(- (Sum z)) + (t /. (ef1 + 1)) is Element of the carrier of f

- (b9 /. (ef1 + 1)) is Element of the carrier of f

(- (Sum z)) + (- (b9 /. (ef1 + 1))) is Element of the carrier of f

(Sum z) + (b9 /. (ef1 + 1)) is Element of the carrier of f

- ((Sum z) + (b9 /. (ef1 + 1))) is Element of the carrier of f

Sum <*(b9 /. (ef1 + 1))*> is Element of the carrier of f

(Sum z) + (Sum <*(b9 /. (ef1 + 1))*>) is Element of the carrier of f

- ((Sum z) + (Sum <*(b9 /. (ef1 + 1))*>)) is Element of the carrier of f

Sum b9 is Element of the carrier of f

- (Sum b9) is Element of the carrier of f

t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

b9 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom t is Element of K19(NAT)

Sum t is Element of the carrier of f

Sum b9 is Element of the carrier of f

- (Sum b9) is Element of the carrier of f

ef1 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom ef1 is Element of K19(NAT)

<*> the carrier of f is Relation-like NAT -defined the carrier of f -valued Function-like functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-like FinSubsequence-like FinSequence-membered integer Function-yielding V54() FinSequence of the carrier of f

Sum ef1 is Element of the carrier of f

0. f is zero Element of the carrier of f

- (0. f) is Element of the carrier of f

Sum t is Element of the carrier of f

- (Sum t) is Element of the carrier of f

ef1 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom ef1 is Element of K19(NAT)

Sum ef1 is Element of the carrier of f

Sum t is Element of the carrier of f

- (Sum t) is Element of the carrier of f

f is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty set

rho is Element of the carrier of f

ef is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum ef is Element of the carrier of f

rho * (Sum ef) is Element of the carrier of f

rho * ef is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum (rho * ef) is Element of the carrier of f

len ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

b9 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Seg ef1 is V40() V47(ef1) Element of K19(NAT)

{ b

b9 | (Seg ef1) is Relation-like NAT -defined the carrier of f -valued Function-like FinSubsequence-like Element of K19(K20(NAT, the carrier of f))

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

len b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 + 1 is non empty V24() V25() V26() V30() complex V32() ext-real positive non negative V40() V45() integer Element of NAT

a1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set

b1 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len b1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

b9 /. (ef1 + 1) is Element of the carrier of f

<*(b9 /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of f

[1,(b9 /. (ef1 + 1))] is set

{[1,(b9 /. (ef1 + 1))]} is non empty V12() V47(1) set

b1 ^ <*(b9 /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

t is Element of the carrier of f

Sum b9 is Element of the carrier of f

t * (Sum b9) is Element of the carrier of f

Sum (b1 ^ <*(b9 /. (ef1 + 1))*>) is Element of the carrier of f

t * (Sum (b1 ^ <*(b9 /. (ef1 + 1))*>)) is Element of the carrier of f

Sum b1 is Element of the carrier of f

Sum <*(b9 /. (ef1 + 1))*> is Element of the carrier of f

(Sum b1) + (Sum <*(b9 /. (ef1 + 1))*>) is Element of the carrier of f

t * ((Sum b1) + (Sum <*(b9 /. (ef1 + 1))*>)) is Element of the carrier of f

t * (Sum b1) is Element of the carrier of f

t * (Sum <*(b9 /. (ef1 + 1))*>) is Element of the carrier of f

(t * (Sum b1)) + (t * (Sum <*(b9 /. (ef1 + 1))*>)) is Element of the carrier of f

t * b1 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum (t * b1) is Element of the carrier of f

(Sum (t * b1)) + (t * (Sum <*(b9 /. (ef1 + 1))*>)) is Element of the carrier of f

t * (b9 /. (ef1 + 1)) is Element of the carrier of f

(Sum (t * b1)) + (t * (b9 /. (ef1 + 1))) is Element of the carrier of f

<*(t * (b9 /. (ef1 + 1)))*> is Relation-like NAT -defined the carrier of f -valued Function-like non empty V12() V40() V47(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of f

[1,(t * (b9 /. (ef1 + 1)))] is set

{[1,(t * (b9 /. (ef1 + 1)))]} is non empty V12() V47(1) set

Sum <*(t * (b9 /. (ef1 + 1)))*> is Element of the carrier of f

(Sum (t * b1)) + (Sum <*(t * (b9 /. (ef1 + 1)))*>) is Element of the carrier of f

t * <*(b9 /. (ef1 + 1))*> is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum (t * <*(b9 /. (ef1 + 1))*>) is Element of the carrier of f

(Sum (t * b1)) + (Sum (t * <*(b9 /. (ef1 + 1))*>)) is Element of the carrier of f

(t * b1) ^ (t * <*(b9 /. (ef1 + 1))*>) is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum ((t * b1) ^ (t * <*(b9 /. (ef1 + 1))*>)) is Element of the carrier of f

t * b9 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum (t * b9) is Element of the carrier of f

b9 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t is Element of the carrier of f

Sum b9 is Element of the carrier of f

t * (Sum b9) is Element of the carrier of f

t * b9 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum (t * b9) is Element of the carrier of f

t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is Element of the carrier of f

ef1 * t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len (ef1 * t) is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

Seg (len (ef1 * t)) is V40() V47( len (ef1 * t)) Element of K19(NAT)

{ b

dom (ef1 * t) is Element of K19(NAT)

dom t is Element of K19(NAT)

Seg (len t) is V40() V47( len t) Element of K19(NAT)

{ b

<*> the carrier of f is Relation-like NAT -defined the carrier of f -valued Function-like functional empty V24() V25() V26() V28() V29() V30() complex V32() ext-real non positive non negative V40() V45() V47( {} ) FinSequence-like FinSubsequence-like FinSequence-membered integer Function-yielding V54() FinSequence of the carrier of f

Sum t is Element of the carrier of f

0. f is zero Element of the carrier of f

ef1 * (Sum t) is Element of the carrier of f

Sum (ef1 * t) is Element of the carrier of f

t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is Element of the carrier of f

Sum t is Element of the carrier of f

ef1 * (Sum t) is Element of the carrier of f

ef1 * t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum (ef1 * t) is Element of the carrier of f

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

f is non empty left_add-cancelable right_add-cancelable right_complementable add-associative right_zeroed V150() V151() V152() V153() addLoopStr

the carrier of f is non empty set

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- (- rho) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

len rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer set

(- (- rho)) . ef is Element of the carrier of f

(- rho) . ef is Element of the carrier of f

- ((- rho) . ef) is Element of the carrier of f

rho . ef is Element of the carrier of f

- (rho . ef) is Element of the carrier of f

- (- (rho . ef)) is Element of the carrier of f

len (- rho) is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

len (- (- rho)) is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

f is non empty left_add-cancelable right_add-cancelable right_complementable add-associative right_zeroed V150() V151() V152() V153() addLoopStr

the carrier of f is non empty set

0_. f is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

0. f is zero Element of the carrier of f

NAT --> (0. f) is Relation-like NAT -defined the carrier of f -valued Function-like constant non empty total V18( NAT , the carrier of f) V28() Element of K19(K20(NAT, the carrier of f))

{(0. f)} is non empty V12() V47(1) set

K20(NAT,{(0. f)}) is V40() set

- (0_. f) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

len (0_. f) is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer set

(0_. f) . ef1 is Element of the carrier of f

(- (0_. f)) . ef1 is Element of the carrier of f

len (- (0_. f)) is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

f is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty set

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

Polynom-Ring f is non empty left_add-cancelable right_add-cancelable right_complementable strict add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of (Polynom-Ring f) is non empty set

rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

ef is Element of the carrier of (Polynom-Ring f)

- ef is Element of the carrier of (Polynom-Ring f)

ef1 is Element of the carrier of (Polynom-Ring f)

t is Element of the carrier of (Polynom-Ring f)

ef + t is Element of the carrier of (Polynom-Ring f)

rho - rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

rho + (- rho) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

0_. f is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

0. f is zero Element of the carrier of f

NAT --> (0. f) is Relation-like NAT -defined the carrier of f -valued Function-like constant non empty total V18( NAT , the carrier of f) V28() Element of K19(K20(NAT, the carrier of f))

{(0. f)} is non empty V12() V47(1) set

K20(NAT,{(0. f)}) is V40() set

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

- t is Element of the carrier of (Polynom-Ring f)

f is non empty left_add-cancelable right_add-cancelable right_complementable add-associative right_zeroed V150() V151() V152() V153() addLoopStr

the carrier of f is non empty set

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- (- rho) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

f is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive Abelian add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty set

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

ef is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

rho + ef is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- (rho + ef) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- ef is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

(- rho) + (- ef) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

Polynom-Ring f is non empty left_add-cancelable right_add-cancelable right_complementable strict right-distributive left-distributive distributive Abelian add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of (Polynom-Ring f) is non empty set

ef1 is Element of the carrier of (Polynom-Ring f)

t is Element of the carrier of (Polynom-Ring f)

ef1 + t is Element of the carrier of (Polynom-Ring f)

- (ef1 + t) is Element of the carrier of (Polynom-Ring f)

- ef1 is Element of the carrier of (Polynom-Ring f)

- t is Element of the carrier of (Polynom-Ring f)

(- ef1) + (- t) is Element of the carrier of (Polynom-Ring f)

f is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive Abelian add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty set

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

ef is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

rho *' ef is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- (rho *' ef) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

(- rho) *' ef is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

- ef is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

rho *' (- ef) is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

Polynom-Ring f is non empty left_add-cancelable right_add-cancelable right_complementable strict right-distributive left-distributive distributive Abelian add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of (Polynom-Ring f) is non empty set

ef1 is Element of the carrier of (Polynom-Ring f)

t is Element of the carrier of (Polynom-Ring f)

ef1 * t is Element of the carrier of (Polynom-Ring f)

- (ef1 * t) is Element of the carrier of (Polynom-Ring f)

- ef1 is Element of the carrier of (Polynom-Ring f)

(- ef1) * t is Element of the carrier of (Polynom-Ring f)

- t is Element of the carrier of (Polynom-Ring f)

ef1 * (- t) is Element of the carrier of (Polynom-Ring f)

f is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

Polynom-Ring f is non empty left_add-cancelable right_add-cancelable right_complementable strict add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of (Polynom-Ring f) is non empty set

the carrier of f is non empty set

rho is Relation-like NAT -defined the carrier of (Polynom-Ring f) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Polynom-Ring f)

len rho is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

Seg (len rho) is V40() V47( len rho) Element of K19(NAT)

{ b

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer set

rho . ef1 is set

rho /. ef1 is Element of the carrier of (Polynom-Ring f)

t is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

t . ef is Element of the carrier of f

dom rho is Element of K19(NAT)

ef1 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

dom ef1 is Element of K19(NAT)

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

rho . t is set

ef1 . t is set

ef1 is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom ef1 is Element of K19(NAT)

t is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

len t is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

dom t is Element of K19(NAT)

Seg (len rho) is V40() V47( len rho) Element of K19(NAT)

{ b

b9 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer set

rho . b9 is set

ef1 . b9 is set

t . b9 is set

zz is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

zz . ef is Element of the carrier of f

a1 is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

a1 . ef is Element of the carrier of f

f is non empty left_add-cancelable right_add-cancelable right_complementable right-distributive left-distributive distributive add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of f is non empty set

K20(NAT, the carrier of f) is V40() set

K19(K20(NAT, the carrier of f)) is V40() set

Polynom-Ring f is non empty left_add-cancelable right_add-cancelable right_complementable strict add-associative right_zeroed V150() V151() V152() V153() doubleLoopStr

the carrier of (Polynom-Ring f) is non empty set

rho is Relation-like NAT -defined the carrier of f -valued Function-like non empty total V18( NAT , the carrier of f) finite-Support Element of K19(K20(NAT, the carrier of f))

ef is Relation-like NAT -defined the carrier of (Polynom-Ring f) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Polynom-Ring f)

Sum ef is Element of the carrier of (Polynom-Ring f)

ef1 is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

rho . ef1 is Element of the carrier of f

(f,ef,ef1) is Relation-like NAT -defined the carrier of f -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of f

Sum (f,ef,ef1) is Element of the carrier of f

len ef is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT

t is V24() V25() V26() V30() complex V32() ext-real non negative