REAL is non empty non trivial non finite V67() V68() V69() V73() set
NAT is ordinal non empty non trivial non finite cardinal limit_cardinal V67() V68() V69() V70() V71() V72() V73() Element of bool REAL
bool REAL is non empty non trivial non finite set
F_Complex is non empty non degenerated non trivial right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital V175() left_unital V185() V186() V187() algebraic-closed domRing-like doubleLoopStr
the carrier of F_Complex is non empty non trivial set
COMPLEX is non empty non trivial non finite V67() V73() set
NAT is ordinal non empty non trivial non finite cardinal limit_cardinal V67() V68() V69() V70() V71() V72() V73() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K227(NAT) is V55() set
RAT is non empty non trivial non finite V67() V68() V69() V70() V73() set
INT is non empty non trivial non finite V67() V68() V69() V70() V71() V73() set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V57() V58() V59() set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:NAT,REAL:] is Relation-like non empty non trivial non finite V57() V58() V59() set
bool [:NAT,REAL:] is non empty non trivial non finite set
[:NAT,COMPLEX:] is Relation-like non empty non trivial non finite V57() set
bool [:NAT,COMPLEX:] is non empty non trivial non finite set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V57() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered rational V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support Element of NAT
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support set
the Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support set is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support set
1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
2 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
K357(0,1,2) is finite V67() V68() V69() V70() V71() V72() set
[:K357(0,1,2),K357(0,1,2):] is Relation-like RAT -valued INT -valued finite V57() V58() V59() V60() set
[:[:K357(0,1,2),K357(0,1,2):],K357(0,1,2):] is Relation-like RAT -valued INT -valued finite V57() V58() V59() V60() set
bool [:[:K357(0,1,2),K357(0,1,2):],K357(0,1,2):] is finite V44() set
bool [:K357(0,1,2),K357(0,1,2):] is finite V44() set
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = 1 } is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V57() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V57() V58() V59() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V57() V58() V59() set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V57() V58() V59() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V57() V58() V59() set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V57() V58() V59() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V57() V58() V59() V60() set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V57() V58() V59() V60() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
3 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
Seg 1 is non empty trivial finite 1 -element V67() V68() V69() V70() V71() V72() Element of bool NAT
PI is V31() real ext-real Element of REAL
PI / 2 is V31() real ext-real Element of REAL
- (PI / 2) is V31() real ext-real Element of REAL
2 * PI is V31() real ext-real Element of REAL
3 / 2 is non empty V31() real ext-real positive non negative Element of REAL
(3 / 2) * PI is V31() real ext-real Element of REAL
<i> is V31() Element of COMPLEX
Arg 1 is V31() real ext-real Element of REAL
addcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like V25([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative V57() Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
multcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like V25([:COMPLEX,COMPLEX:], COMPLEX ) commutative associative V57() Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
1r is V31() Element of COMPLEX
0c is Relation-like non-empty empty-yielding NAT -defined RAT -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support Element of COMPLEX
0. F_Complex is V31() zero right_complementable Element of the carrier of F_Complex
the ZeroF of F_Complex is V31() right_complementable Element of the carrier of F_Complex
1_ F_Complex is V31() right_complementable Element of the carrier of F_Complex
1. F_Complex is V31() non zero right_complementable Element of the carrier of F_Complex
the OneF of F_Complex is V31() right_complementable Element of the carrier of F_Complex
|.(1. F_Complex).| is V31() real ext-real Element of REAL
Re (1. F_Complex) is V31() real ext-real Element of REAL
(Re (1. F_Complex)) ^2 is V31() real ext-real Element of REAL
K104((Re (1. F_Complex)),(Re (1. F_Complex))) is V31() real ext-real set
Im (1. F_Complex) is V31() real ext-real Element of REAL
(Im (1. F_Complex)) ^2 is V31() real ext-real Element of REAL
K104((Im (1. F_Complex)),(Im (1. F_Complex))) is V31() real ext-real set
((Re (1. F_Complex)) ^2) + ((Im (1. F_Complex)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (1. F_Complex)) ^2) + ((Im (1. F_Complex)) ^2)) is V31() real ext-real Element of REAL
power F_Complex is Relation-like [: the carrier of F_Complex,NAT:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex,NAT:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex,NAT:], the carrier of F_Complex:]
[: the carrier of F_Complex,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V57() V58() V59() V60() set
[:[: the carrier of F_Complex,NAT:], the carrier of F_Complex:] is Relation-like non empty non trivial non finite set
bool [:[: the carrier of F_Complex,NAT:], the carrier of F_Complex:] is non empty non trivial non finite set
|.1r.| is V31() real ext-real Element of REAL
Re 1r is V31() real ext-real Element of REAL
(Re 1r) ^2 is V31() real ext-real Element of REAL
K104((Re 1r),(Re 1r)) is V31() real ext-real set
Im 1r is V31() real ext-real Element of REAL
(Im 1r) ^2 is V31() real ext-real Element of REAL
K104((Im 1r),(Im 1r)) is V31() real ext-real set
((Re 1r) ^2) + ((Im 1r) ^2) is V31() real ext-real Element of REAL
sqrt (((Re 1r) ^2) + ((Im 1r) ^2)) is V31() real ext-real Element of REAL
sin is Relation-like REAL -defined REAL -valued Function-like V25( REAL , REAL ) V57() V58() V59() Element of bool [:REAL,REAL:]
cos is Relation-like REAL -defined REAL -valued Function-like V25( REAL , REAL ) V57() V58() V59() Element of bool [:REAL,REAL:]
K706(cos,0) is V31() real ext-real Element of REAL
K706(sin,0) is V31() real ext-real Element of REAL
cos 0 is V31() real ext-real Element of REAL
sin 0 is V31() real ext-real Element of REAL
cos (PI / 2) is V31() real ext-real Element of REAL
sin (PI / 2) is V31() real ext-real Element of REAL
cos PI is V31() real ext-real Element of REAL
- 1 is non empty V31() real ext-real non positive negative integer Element of REAL
sin PI is V31() real ext-real Element of REAL
PI + (PI / 2) is V31() real ext-real Element of REAL
cos (PI + (PI / 2)) is V31() real ext-real Element of REAL
sin (PI + (PI / 2)) is V31() real ext-real Element of REAL
cos (2 * PI) is V31() real ext-real Element of REAL
sin (2 * PI) is V31() real ext-real Element of REAL
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support FinSequence of REAL
Product (<*> REAL) is V31() real ext-real Element of REAL
K105(1) is non empty V31() real ext-real non positive negative integer set
{{}} is functional non empty trivial finite V44() 1 -element V67() V68() V69() V70() V71() V72() set
Z_3 is strict doubleLoopStr
add3 is Relation-like [:K357(0,1,2),K357(0,1,2):] -defined K357(0,1,2) -valued Function-like V25([:K357(0,1,2),K357(0,1,2):],K357(0,1,2)) finite V57() V58() V59() V60() finite-support Element of bool [:[:K357(0,1,2),K357(0,1,2):],K357(0,1,2):]
mult3 is Relation-like [:K357(0,1,2),K357(0,1,2):] -defined K357(0,1,2) -valued Function-like V25([:K357(0,1,2),K357(0,1,2):],K357(0,1,2)) finite V57() V58() V59() V60() finite-support Element of bool [:[:K357(0,1,2),K357(0,1,2):],K357(0,1,2):]
unit3 is ordinal natural V31() real ext-real non negative integer finite cardinal rational Element of K357(0,1,2)
zero3 is ordinal natural V31() real ext-real non negative integer finite cardinal rational Element of K357(0,1,2)
doubleLoopStr(# K357(0,1,2),add3,mult3,unit3,zero3 #) is strict doubleLoopStr
MGFC is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
0 + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
MGFC is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
cMGFC is ordinal natural V31() real ext-real non negative integer finite cardinal set
n is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
S is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
fs is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
cMGFC is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
MGFC is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len MGFC is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
MGFC | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined Function-like finite FinSubsequence-like finite-support set
MGFC . 1 is set
<*(MGFC . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
Seg (len MGFC) is finite len MGFC -element V67() V68() V69() V70() V71() V72() Element of bool NAT
dom MGFC is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
0 + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(MGFC | (Seg 1)) . 1 is set
cMGFC is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom cMGFC is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
len cMGFC is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
MGFC is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
n is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
cMGFC is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
Seg cMGFC is finite cMGFC -element V67() V68() V69() V70() V71() V72() Element of bool NAT
MGFC | (Seg cMGFC) is Relation-like NAT -defined Seg cMGFC -defined NAT -defined Function-like finite FinSubsequence-like finite-support set
Seg n is finite n -element V67() V68() V69() V70() V71() V72() Element of bool NAT
(MGFC | (Seg cMGFC)) | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined Function-like finite FinSubsequence-like finite-support set
MGFC | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined Function-like finite FinSubsequence-like finite-support set
n is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
n + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
S is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
len S is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom S is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Product S is V31() right_complementable Element of the carrier of F_Complex
the multF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) associative Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
K228( the carrier of F_Complex,S, the multF of F_Complex) is V31() right_complementable Element of the carrier of F_Complex
|.(Product S).| is V31() real ext-real Element of REAL
Re (Product S) is V31() real ext-real Element of REAL
(Re (Product S)) ^2 is V31() real ext-real Element of REAL
K104((Re (Product S)),(Re (Product S))) is V31() real ext-real set
Im (Product S) is V31() real ext-real Element of REAL
(Im (Product S)) ^2 is V31() real ext-real Element of REAL
K104((Im (Product S)),(Im (Product S))) is V31() real ext-real set
((Re (Product S)) ^2) + ((Im (Product S)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (Product S)) ^2) + ((Im (Product S)) ^2)) is V31() real ext-real Element of REAL
fs is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len fs is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
Product fs is V31() real ext-real Element of REAL
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
qc is V31() real ext-real Element of REAL
<*qc*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like V57() V58() V59() V61() V62() V63() V64() finite-support Element of REAL *
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
q ^ <*qc*> is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len q is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
len <*qc*> is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len q) + (len <*qc*>) is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len q) + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
fs . (len S) is V31() real ext-real set
p1 is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
ps is V31() right_complementable Element of the carrier of F_Complex
<*ps*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of the carrier of F_Complex *
the carrier of F_Complex * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Complex
p1 ^ <*ps*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
len p1 is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
len <*ps*> is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len p1) + (len <*ps*>) is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len p1) + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom p1 is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
dom q is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
qi is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
p1 /. qi is V31() right_complementable Element of the carrier of F_Complex
p1 . qi is set
S . qi is set
S /. qi is V31() right_complementable Element of the carrier of F_Complex
|.(p1 /. qi).| is V31() real ext-real Element of REAL
Re (p1 /. qi) is V31() real ext-real Element of REAL
(Re (p1 /. qi)) ^2 is V31() real ext-real Element of REAL
K104((Re (p1 /. qi)),(Re (p1 /. qi))) is V31() real ext-real set
Im (p1 /. qi) is V31() real ext-real Element of REAL
(Im (p1 /. qi)) ^2 is V31() real ext-real Element of REAL
K104((Im (p1 /. qi)),(Im (p1 /. qi))) is V31() real ext-real set
((Re (p1 /. qi)) ^2) + ((Im (p1 /. qi)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (p1 /. qi)) ^2) + ((Im (p1 /. qi)) ^2)) is V31() real ext-real Element of REAL
fs . qi is V31() real ext-real set
q . qi is V31() real ext-real set
Product p1 is V31() right_complementable Element of the carrier of F_Complex
K228( the carrier of F_Complex,p1, the multF of F_Complex) is V31() right_complementable Element of the carrier of F_Complex
Product q is V31() real ext-real Element of REAL
(Product q) * qc is V31() real ext-real Element of REAL
S /. (len S) is V31() right_complementable Element of the carrier of F_Complex
S . (len S) is set
i is V31() Element of COMPLEX
|.i.| is V31() real ext-real Element of REAL
Re i is V31() real ext-real Element of REAL
(Re i) ^2 is V31() real ext-real Element of REAL
K104((Re i),(Re i)) is V31() real ext-real set
Im i is V31() real ext-real Element of REAL
(Im i) ^2 is V31() real ext-real Element of REAL
K104((Im i),(Im i)) is V31() real ext-real set
((Re i) ^2) + ((Im i) ^2) is V31() real ext-real Element of REAL
sqrt (((Re i) ^2) + ((Im i) ^2)) is V31() real ext-real Element of REAL
(Product p1) * ps is V31() right_complementable Element of the carrier of F_Complex
the multF of F_Complex . ((Product p1),ps) is V31() right_complementable Element of the carrier of F_Complex
[(Product p1),ps] is non empty set
{(Product p1),ps} is non empty finite V67() set
{(Product p1)} is non empty trivial finite 1 -element V67() set
{{(Product p1),ps},{(Product p1)}} is non empty finite V44() set
the multF of F_Complex . [(Product p1),ps] is set
(Product p1) * ps is V31() Element of COMPLEX
qi is V31() Element of COMPLEX
|.qi.| is V31() real ext-real Element of REAL
Re qi is V31() real ext-real Element of REAL
(Re qi) ^2 is V31() real ext-real Element of REAL
K104((Re qi),(Re qi)) is V31() real ext-real set
Im qi is V31() real ext-real Element of REAL
(Im qi) ^2 is V31() real ext-real Element of REAL
K104((Im qi),(Im qi)) is V31() real ext-real set
((Re qi) ^2) + ((Im qi) ^2) is V31() real ext-real Element of REAL
sqrt (((Re qi) ^2) + ((Im qi) ^2)) is V31() real ext-real Element of REAL
|.qi.| * |.i.| is V31() real ext-real Element of REAL
n is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
len n is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom n is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Product n is V31() right_complementable Element of the carrier of F_Complex
the multF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) associative Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
K228( the carrier of F_Complex,n, the multF of F_Complex) is V31() right_complementable Element of the carrier of F_Complex
|.(Product n).| is V31() real ext-real Element of REAL
Re (Product n) is V31() real ext-real Element of REAL
(Re (Product n)) ^2 is V31() real ext-real Element of REAL
K104((Re (Product n)),(Re (Product n))) is V31() real ext-real set
Im (Product n) is V31() real ext-real Element of REAL
(Im (Product n)) ^2 is V31() real ext-real Element of REAL
K104((Im (Product n)),(Im (Product n))) is V31() real ext-real set
((Re (Product n)) ^2) + ((Im (Product n)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (Product n)) ^2) + ((Im (Product n)) ^2)) is V31() real ext-real Element of REAL
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len S is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
Product S is V31() real ext-real Element of REAL
<*> the carrier of F_Complex is Relation-like non-empty empty-yielding NAT -defined the carrier of F_Complex -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support Element of the carrier of F_Complex *
the carrier of F_Complex * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Complex
n is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
len n is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom n is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Product n is V31() right_complementable Element of the carrier of F_Complex
the multF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) associative Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
K228( the carrier of F_Complex,n, the multF of F_Complex) is V31() right_complementable Element of the carrier of F_Complex
|.(Product n).| is V31() real ext-real Element of REAL
Re (Product n) is V31() real ext-real Element of REAL
(Re (Product n)) ^2 is V31() real ext-real Element of REAL
K104((Re (Product n)),(Re (Product n))) is V31() real ext-real set
Im (Product n) is V31() real ext-real Element of REAL
(Im (Product n)) ^2 is V31() real ext-real Element of REAL
K104((Im (Product n)),(Im (Product n))) is V31() real ext-real set
((Re (Product n)) ^2) + ((Im (Product n)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (Product n)) ^2) + ((Im (Product n)) ^2)) is V31() real ext-real Element of REAL
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len S is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
Product S is V31() real ext-real Element of REAL
bool the carrier of F_Complex is set
cMGFC is non empty finite Element of bool the carrier of F_Complex
card cMGFC is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
canFS cMGFC is Relation-like NAT -defined cMGFC -valued Function-like one-to-one non empty V26(cMGFC) finite FinSequence-like FinSubsequence-like finite-support FinSequence of cMGFC
(cMGFC,1) -bag is Relation-like the carrier of F_Complex -defined RAT -valued Function-like total V57() V58() V59() V60() finite-support Element of Bags the carrier of F_Complex
Bags the carrier of F_Complex is non empty set
Bags the carrier of F_Complex is functional non empty Element of bool (Bags the carrier of F_Complex)
bool (Bags the carrier of F_Complex) is set
poly_with_roots ((cMGFC,1) -bag) is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V25( NAT , the carrier of F_Complex) finite-Support Element of bool [:NAT, the carrier of F_Complex:]
[:NAT, the carrier of F_Complex:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of F_Complex:] is non empty non trivial non finite set
n is V31() right_complementable Element of the carrier of F_Complex
eval ((poly_with_roots ((cMGFC,1) -bag)),n) is V31() right_complementable Element of the carrier of F_Complex
|.(eval ((poly_with_roots ((cMGFC,1) -bag)),n)).| is V31() real ext-real Element of REAL
Re (eval ((poly_with_roots ((cMGFC,1) -bag)),n)) is V31() real ext-real Element of REAL
(Re (eval ((poly_with_roots ((cMGFC,1) -bag)),n))) ^2 is V31() real ext-real Element of REAL
K104((Re (eval ((poly_with_roots ((cMGFC,1) -bag)),n))),(Re (eval ((poly_with_roots ((cMGFC,1) -bag)),n)))) is V31() real ext-real set
Im (eval ((poly_with_roots ((cMGFC,1) -bag)),n)) is V31() real ext-real Element of REAL
(Im (eval ((poly_with_roots ((cMGFC,1) -bag)),n))) ^2 is V31() real ext-real Element of REAL
K104((Im (eval ((poly_with_roots ((cMGFC,1) -bag)),n))),(Im (eval ((poly_with_roots ((cMGFC,1) -bag)),n)))) is V31() real ext-real set
((Re (eval ((poly_with_roots ((cMGFC,1) -bag)),n))) ^2) + ((Im (eval ((poly_with_roots ((cMGFC,1) -bag)),n))) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (eval ((poly_with_roots ((cMGFC,1) -bag)),n))) ^2) + ((Im (eval ((poly_with_roots ((cMGFC,1) -bag)),n))) ^2)) is V31() real ext-real Element of REAL
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len S is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom S is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Product S is V31() real ext-real Element of REAL
len (canFS cMGFC) is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom (canFS cMGFC) is non empty finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Seg (card cMGFC) is non empty finite card cMGFC -element V67() V68() V69() V70() V71() V72() Element of bool NAT
fs is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(canFS cMGFC) . fs is set
qc is V31() right_complementable Element of the carrier of F_Complex
- qc is V31() right_complementable Element of the carrier of F_Complex
<%(- qc),(1_ F_Complex)%> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V25( NAT , the carrier of F_Complex) finite-Support Element of bool [:NAT, the carrier of F_Complex:]
eval (<%(- qc),(1_ F_Complex)%>,n) is V31() right_complementable Element of the carrier of F_Complex
p1 is V31() right_complementable Element of the carrier of F_Complex
fs is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
dom fs is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
q is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
qc is V31() right_complementable Element of the carrier of F_Complex
(canFS cMGFC) . q is set
fs /. q is V31() right_complementable Element of the carrier of F_Complex
fs . q is set
- qc is V31() right_complementable Element of the carrier of F_Complex
<%(- qc),(1_ F_Complex)%> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V25( NAT , the carrier of F_Complex) finite-Support Element of bool [:NAT, the carrier of F_Complex:]
eval (<%(- qc),(1_ F_Complex)%>,n) is V31() right_complementable Element of the carrier of F_Complex
p1 is V31() right_complementable Element of the carrier of F_Complex
- p1 is V31() right_complementable Element of the carrier of F_Complex
<%(- p1),(1_ F_Complex)%> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V25( NAT , the carrier of F_Complex) finite-Support Element of bool [:NAT, the carrier of F_Complex:]
eval (<%(- p1),(1_ F_Complex)%>,n) is V31() right_complementable Element of the carrier of F_Complex
q is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
fs /. q is V31() right_complementable Element of the carrier of F_Complex
|.(fs /. q).| is V31() real ext-real Element of REAL
Re (fs /. q) is V31() real ext-real Element of REAL
(Re (fs /. q)) ^2 is V31() real ext-real Element of REAL
K104((Re (fs /. q)),(Re (fs /. q))) is V31() real ext-real set
Im (fs /. q) is V31() real ext-real Element of REAL
(Im (fs /. q)) ^2 is V31() real ext-real Element of REAL
K104((Im (fs /. q)),(Im (fs /. q))) is V31() real ext-real set
((Re (fs /. q)) ^2) + ((Im (fs /. q)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (fs /. q)) ^2) + ((Im (fs /. q)) ^2)) is V31() real ext-real Element of REAL
S . q is V31() real ext-real set
(canFS cMGFC) . q is set
fs . q is set
p1 is V31() right_complementable Element of the carrier of F_Complex
- p1 is V31() right_complementable Element of the carrier of F_Complex
<%(- p1),(1_ F_Complex)%> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like V25( NAT , the carrier of F_Complex) finite-Support Element of bool [:NAT, the carrier of F_Complex:]
eval (<%(- p1),(1_ F_Complex)%>,n) is V31() right_complementable Element of the carrier of F_Complex
(- p1) + n is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
the addF of F_Complex . ((- p1),n) is V31() right_complementable Element of the carrier of F_Complex
[(- p1),n] is non empty set
{(- p1),n} is non empty finite V67() set
{(- p1)} is non empty trivial finite 1 -element V67() set
{{(- p1),n},{(- p1)}} is non empty finite V44() set
the addF of F_Complex . [(- p1),n] is set
(- p1) + n is V31() Element of COMPLEX
n - p1 is V31() right_complementable Element of the carrier of F_Complex
n + (- p1) is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex . (n,(- p1)) is V31() right_complementable Element of the carrier of F_Complex
[n,(- p1)] is non empty set
{n,(- p1)} is non empty finite V67() set
{n} is non empty trivial finite 1 -element V67() set
{{n,(- p1)},{n}} is non empty finite V44() set
the addF of F_Complex . [n,(- p1)] is set
n + (- p1) is V31() Element of COMPLEX
len fs is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
Product fs is V31() right_complementable Element of the carrier of F_Complex
the multF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) associative Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
K228( the carrier of F_Complex,fs, the multF of F_Complex) is V31() right_complementable Element of the carrier of F_Complex
cMGFC is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
dom cMGFC is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Sum cMGFC is V31() right_complementable Element of the carrier of F_Complex
n is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
n + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
S is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
len S is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom S is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Sum S is V31() right_complementable Element of the carrier of F_Complex
fs is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
q is V31() right_complementable Element of the carrier of F_Complex
<*q*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support Element of the carrier of F_Complex *
the carrier of F_Complex * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Complex
fs ^ <*q*> is Relation-like NAT -defined the carrier of F_Complex -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
dom fs is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
qc is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
S . qc is set
fs . qc is set
0 + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
S . (len S) is set
Sum fs is V31() right_complementable Element of the carrier of F_Complex
len fs is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
len <*q*> is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len fs) + (len <*q*>) is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len fs) + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
qc is V31() Element of COMPLEX
p1 is V31() Element of COMPLEX
Sum <*q*> is V31() right_complementable Element of the carrier of F_Complex
(Sum fs) + (Sum <*q*>) is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
the addF of F_Complex . ((Sum fs),(Sum <*q*>)) is V31() right_complementable Element of the carrier of F_Complex
[(Sum fs),(Sum <*q*>)] is non empty set
{(Sum fs),(Sum <*q*>)} is non empty finite V67() set
{(Sum fs)} is non empty trivial finite 1 -element V67() set
{{(Sum fs),(Sum <*q*>)},{(Sum fs)}} is non empty finite V44() set
the addF of F_Complex . [(Sum fs),(Sum <*q*>)] is set
(Sum fs) + (Sum <*q*>) is V31() Element of COMPLEX
ps is V31() real ext-real integer set
qi is V31() real ext-real integer set
ps + qi is V31() real ext-real integer rational Element of INT
len cMGFC is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
n is Relation-like NAT -defined the carrier of F_Complex -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of F_Complex
len n is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom n is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Sum n is V31() right_complementable Element of the carrier of F_Complex
<*> the carrier of F_Complex is Relation-like non-empty empty-yielding NAT -defined the carrier of F_Complex -valued ordinal natural Function-like one-to-one constant functional empty trivial V31() real ext-real non positive non negative integer V38() finite finite-yielding V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V57() V58() V59() V60() V61() V62() V63() V64() V67() V68() V69() V70() V71() V72() V73() FinSequence-yielding finite-support Element of the carrier of F_Complex *
the carrier of F_Complex * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Complex
n is V31() real ext-real Element of REAL
MGFC is V31() right_complementable Element of the carrier of F_Complex
S is V31() real ext-real Element of REAL
cMGFC is V31() right_complementable Element of the carrier of F_Complex
n * S is V31() real ext-real Element of REAL
MGFC * cMGFC is V31() right_complementable Element of the carrier of F_Complex
the multF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) associative Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
the multF of F_Complex . (MGFC,cMGFC) is V31() right_complementable Element of the carrier of F_Complex
[MGFC,cMGFC] is non empty set
{MGFC,cMGFC} is non empty finite V67() set
{MGFC} is non empty trivial finite 1 -element V67() set
{{MGFC,cMGFC},{MGFC}} is non empty finite V44() set
the multF of F_Complex . [MGFC,cMGFC] is set
MGFC * cMGFC is V31() Element of COMPLEX
n + S is V31() real ext-real Element of REAL
MGFC + cMGFC is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
the addF of F_Complex . (MGFC,cMGFC) is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex . [MGFC,cMGFC] is set
MGFC + cMGFC is V31() Element of COMPLEX
[**1,0**] is V31() right_complementable Element of the carrier of F_Complex
K104(0,<i>) is V31() set
K103(1,K104(0,<i>)) is V31() set
MGFC is V31() real ext-real Element of REAL
[**MGFC,0**] is V31() right_complementable Element of the carrier of F_Complex
K103(MGFC,K104(0,<i>)) is V31() set
MGFC - 1 is V31() real ext-real Element of REAL
cMGFC is V31() right_complementable Element of the carrier of F_Complex
|.cMGFC.| is V31() real ext-real Element of REAL
Re cMGFC is V31() real ext-real Element of REAL
(Re cMGFC) ^2 is V31() real ext-real Element of REAL
K104((Re cMGFC),(Re cMGFC)) is V31() real ext-real set
Im cMGFC is V31() real ext-real Element of REAL
(Im cMGFC) ^2 is V31() real ext-real Element of REAL
K104((Im cMGFC),(Im cMGFC)) is V31() real ext-real set
((Re cMGFC) ^2) + ((Im cMGFC) ^2) is V31() real ext-real Element of REAL
sqrt (((Re cMGFC) ^2) + ((Im cMGFC) ^2)) is V31() real ext-real Element of REAL
[**MGFC,0**] - cMGFC is V31() right_complementable Element of the carrier of F_Complex
- cMGFC is V31() right_complementable Element of the carrier of F_Complex
[**MGFC,0**] + (- cMGFC) is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex is Relation-like [: the carrier of F_Complex, the carrier of F_Complex:] -defined the carrier of F_Complex -valued Function-like V25([: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex) Element of bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:]
[: the carrier of F_Complex, the carrier of F_Complex:] is Relation-like set
[:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is Relation-like set
bool [:[: the carrier of F_Complex, the carrier of F_Complex:], the carrier of F_Complex:] is set
the addF of F_Complex . ([**MGFC,0**],(- cMGFC)) is V31() right_complementable Element of the carrier of F_Complex
[[**MGFC,0**],(- cMGFC)] is non empty set
{[**MGFC,0**],(- cMGFC)} is non empty finite V67() set
{[**MGFC,0**]} is non empty trivial finite 1 -element V67() set
{{[**MGFC,0**],(- cMGFC)},{[**MGFC,0**]}} is non empty finite V44() set
the addF of F_Complex . [[**MGFC,0**],(- cMGFC)] is set
[**MGFC,0**] + (- cMGFC) is V31() Element of COMPLEX
|.([**MGFC,0**] - cMGFC).| is V31() real ext-real Element of REAL
Re ([**MGFC,0**] - cMGFC) is V31() real ext-real Element of REAL
(Re ([**MGFC,0**] - cMGFC)) ^2 is V31() real ext-real Element of REAL
K104((Re ([**MGFC,0**] - cMGFC)),(Re ([**MGFC,0**] - cMGFC))) is V31() real ext-real set
Im ([**MGFC,0**] - cMGFC) is V31() real ext-real Element of REAL
(Im ([**MGFC,0**] - cMGFC)) ^2 is V31() real ext-real Element of REAL
K104((Im ([**MGFC,0**] - cMGFC)),(Im ([**MGFC,0**] - cMGFC))) is V31() real ext-real set
((Re ([**MGFC,0**] - cMGFC)) ^2) + ((Im ([**MGFC,0**] - cMGFC)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re ([**MGFC,0**] - cMGFC)) ^2) + ((Im ([**MGFC,0**] - cMGFC)) ^2)) is V31() real ext-real Element of REAL
((Re cMGFC) ^2) + ((Im cMGFC) ^2) is V31() real ext-real Element of REAL
1 ^2 is V31() real ext-real Element of REAL
K104(1,1) is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal set
2 * MGFC is V31() real ext-real Element of REAL
(2 * MGFC) * (Re cMGFC) is V31() real ext-real Element of REAL
- ((2 * MGFC) * (Re cMGFC)) is V31() real ext-real Element of REAL
- (2 * MGFC) is V31() real ext-real Element of REAL
MGFC ^2 is V31() real ext-real Element of REAL
K104(MGFC,MGFC) is V31() real ext-real set
(- ((2 * MGFC) * (Re cMGFC))) + (MGFC ^2) is V31() real ext-real Element of REAL
(- (2 * MGFC)) + (MGFC ^2) is V31() real ext-real Element of REAL
(MGFC ^2) - ((2 * MGFC) * (Re cMGFC)) is V31() real ext-real Element of REAL
((MGFC ^2) - ((2 * MGFC) * (Re cMGFC))) + 1 is V31() real ext-real Element of REAL
(MGFC ^2) - (2 * MGFC) is V31() real ext-real Element of REAL
((MGFC ^2) - (2 * MGFC)) + 1 is V31() real ext-real Element of REAL
MGFC - (Re cMGFC) is V31() real ext-real Element of REAL
- (Im cMGFC) is V31() real ext-real Element of REAL
[**(MGFC - (Re cMGFC)),(- (Im cMGFC))**] is V31() right_complementable Element of the carrier of F_Complex
K104((- (Im cMGFC)),<i>) is V31() set
K103((MGFC - (Re cMGFC)),K104((- (Im cMGFC)),<i>)) is V31() set
Re [**(MGFC - (Re cMGFC)),(- (Im cMGFC))**] is V31() real ext-real Element of REAL
Im [**(MGFC - (Re cMGFC)),(- (Im cMGFC))**] is V31() real ext-real Element of REAL
fs is V31() right_complementable Element of the carrier of F_Complex
fs - cMGFC is V31() right_complementable Element of the carrier of F_Complex
fs + (- cMGFC) is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex . (fs,(- cMGFC)) is V31() right_complementable Element of the carrier of F_Complex
[fs,(- cMGFC)] is non empty set
{fs,(- cMGFC)} is non empty finite V67() set
{fs} is non empty trivial finite 1 -element V67() set
{{fs,(- cMGFC)},{fs}} is non empty finite V44() set
the addF of F_Complex . [fs,(- cMGFC)] is set
fs + (- cMGFC) is V31() Element of COMPLEX
|.(fs - cMGFC).| is V31() real ext-real Element of REAL
Re (fs - cMGFC) is V31() real ext-real Element of REAL
(Re (fs - cMGFC)) ^2 is V31() real ext-real Element of REAL
K104((Re (fs - cMGFC)),(Re (fs - cMGFC))) is V31() real ext-real set
Im (fs - cMGFC) is V31() real ext-real Element of REAL
(Im (fs - cMGFC)) ^2 is V31() real ext-real Element of REAL
K104((Im (fs - cMGFC)),(Im (fs - cMGFC))) is V31() real ext-real set
((Re (fs - cMGFC)) ^2) + ((Im (fs - cMGFC)) ^2) is V31() real ext-real Element of REAL
sqrt (((Re (fs - cMGFC)) ^2) + ((Im (fs - cMGFC)) ^2)) is V31() real ext-real Element of REAL
|.(fs - cMGFC).| ^2 is V31() real ext-real Element of REAL
K104(|.(fs - cMGFC).|,|.(fs - cMGFC).|) is V31() real ext-real set
[**(Re cMGFC),(Im cMGFC)**] is V31() right_complementable Element of the carrier of F_Complex
K104((Im cMGFC),<i>) is V31() set
K103((Re cMGFC),K104((Im cMGFC),<i>)) is V31() set
[**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**] is V31() right_complementable Element of the carrier of F_Complex
- [**(Re cMGFC),(Im cMGFC)**] is V31() right_complementable Element of the carrier of F_Complex
[**MGFC,0**] + (- [**(Re cMGFC),(Im cMGFC)**]) is V31() right_complementable Element of the carrier of F_Complex
the addF of F_Complex . ([**MGFC,0**],(- [**(Re cMGFC),(Im cMGFC)**])) is V31() right_complementable Element of the carrier of F_Complex
[[**MGFC,0**],(- [**(Re cMGFC),(Im cMGFC)**])] is non empty set
{[**MGFC,0**],(- [**(Re cMGFC),(Im cMGFC)**])} is non empty finite V67() set
{{[**MGFC,0**],(- [**(Re cMGFC),(Im cMGFC)**])},{[**MGFC,0**]}} is non empty finite V44() set
the addF of F_Complex . [[**MGFC,0**],(- [**(Re cMGFC),(Im cMGFC)**])] is set
[**MGFC,0**] + (- [**(Re cMGFC),(Im cMGFC)**]) is V31() Element of COMPLEX
|.([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]).| is V31() real ext-real Element of REAL
Re ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]) is V31() real ext-real Element of REAL
(Re ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])) ^2 is V31() real ext-real Element of REAL
K104((Re ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])),(Re ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]))) is V31() real ext-real set
Im ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]) is V31() real ext-real Element of REAL
(Im ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])) ^2 is V31() real ext-real Element of REAL
K104((Im ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])),(Im ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]))) is V31() real ext-real set
((Re ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])) ^2) + ((Im ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])) ^2) is V31() real ext-real Element of REAL
sqrt (((Re ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])) ^2) + ((Im ([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**])) ^2)) is V31() real ext-real Element of REAL
|.([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]).| ^2 is V31() real ext-real Element of REAL
K104(|.([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]).|,|.([**MGFC,0**] - [**(Re cMGFC),(Im cMGFC)**]).|) is V31() real ext-real set
0 - (Im cMGFC) is V31() real ext-real Element of REAL
[**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**] is V31() right_complementable Element of the carrier of F_Complex
K104((0 - (Im cMGFC)),<i>) is V31() set
K103((MGFC - (Re cMGFC)),K104((0 - (Im cMGFC)),<i>)) is V31() set
|.[**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**].| is V31() real ext-real Element of REAL
Re [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**] is V31() real ext-real Element of REAL
(Re [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]) ^2 is V31() real ext-real Element of REAL
K104((Re [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]),(Re [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**])) is V31() real ext-real set
Im [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**] is V31() real ext-real Element of REAL
(Im [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]) ^2 is V31() real ext-real Element of REAL
K104((Im [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]),(Im [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**])) is V31() real ext-real set
((Re [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]) ^2) + ((Im [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]) ^2) is V31() real ext-real Element of REAL
sqrt (((Re [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]) ^2) + ((Im [**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**]) ^2)) is V31() real ext-real Element of REAL
|.[**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**].| ^2 is V31() real ext-real Element of REAL
K104(|.[**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**].|,|.[**(MGFC - (Re cMGFC)),(0 - (Im cMGFC))**].|) is V31() real ext-real set
(MGFC - (Re cMGFC)) ^2 is V31() real ext-real Element of REAL
K104((MGFC - (Re cMGFC)),(MGFC - (Re cMGFC))) is V31() real ext-real set
((MGFC - (Re cMGFC)) ^2) + ((Im cMGFC) ^2) is V31() real ext-real Element of REAL
(MGFC - 1) ^2 is V31() real ext-real Element of REAL
K104((MGFC - 1),(MGFC - 1)) is V31() real ext-real set
MGFC is Relation-like NAT -defined REAL -valued Function-like non empty finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
dom MGFC is non empty finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Product MGFC is V31() real ext-real Element of REAL
cMGFC is V31() real ext-real Element of REAL
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
S is set
<*S*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
n ^ <*S*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
rng <*S*> is non empty trivial finite 1 -element set
{S} is non empty trivial finite 1 -element set
fs is V31() real ext-real Element of REAL
q is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
q + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
qc is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len qc is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom qc is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
Product qc is V31() real ext-real Element of REAL
(Product qc) * fs is V31() real ext-real Element of REAL
p1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
ps is set
<*ps*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like finite-support set
p1 ^ <*ps*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set
i is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
rng i is finite V67() V68() V69() Element of bool REAL
{ps} is non empty trivial finite 1 -element set
qi is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len qi is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
len i is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len qi) + (len i) is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len qi) + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
qc . (len qc) is V31() real ext-real set
x is V31() real ext-real Element of REAL
Seg (len qc) is finite len qc -element V67() V68() V69() V70() V71() V72() Element of bool NAT
cMGFC * x is V31() real ext-real Element of REAL
dom qi is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
lc is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
qi . lc is V31() real ext-real set
qc . lc is V31() real ext-real set
Product qi is V31() real ext-real Element of REAL
(Product qi) * x is V31() real ext-real Element of REAL
(Product qi) * fs is V31() real ext-real Element of REAL
((Product qi) * fs) * x is V31() real ext-real Element of REAL
len MGFC is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
Seg (len MGFC) is non empty finite len MGFC -element V67() V68() V69() V70() V71() V72() Element of bool NAT
q is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
dom q is finite V67() V68() V69() V70() V71() V72() Element of bool NAT
qc is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
q . qc is V31() real ext-real set
MGFC . qc is V31() real ext-real set
len q is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
len n is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
len <*S*> is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len n) + (len <*S*>) is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
(len n) + 1 is ordinal natural non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
MGFC . (len MGFC) is V31() real ext-real set
qc is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V57() V58() V59() finite-support FinSequence of REAL
len qc is ordinal natural V31() real ext-real non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT
dom qc is finite V67() V68() V69()