:: 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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty V12() V47(1) set
Seg 2 is non empty V40() V47(2) Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= ef1 ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= (len b9) + (len <*(rho /. (ef1 + 1))*>) ) } is set
Seg (ef1 + 1) is non empty V40() V47(ef1 + 1) Element of K19(NAT)
{ b₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= ef1 + 1 ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len rho ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= ef ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len b19 ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len ef1 ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= ef1 ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len z ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= ef1 ) } is 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))
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len (ef1 * t) ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len t ) } is set
<*> 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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len rho ) } is set
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₁ where b₁ is V24() V25() V26() V30() complex V32() ext-real non negative V40() V45() integer Element of NAT : ( 1 <= b₁ & b₁ <= len rho ) } is set
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