:: UNIROOTS semantic presentation

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

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
is Relation-like non empty non trivial non finite V57() V58() V59() set
bool is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V57() V58() V59() set
bool is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V57() set
bool is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V57() set
bool is non empty non trivial non finite set

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

{ } is set

bool is non empty non trivial non finite set
is Relation-like non empty non trivial non finite V57() V58() V59() set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial non finite V57() V58() V59() set
bool is non empty non trivial non finite set
is Relation-like RAT -valued non empty non trivial non finite V57() V58() V59() set
bool is non empty non trivial non finite set

bool is non empty non trivial non finite set

bool is non empty non trivial non finite set
is Relation-like RAT -valued INT -valued non empty non trivial non finite V57() V58() V59() V60() set
is Relation-like RAT -valued INT -valued non empty non trivial non finite V57() V58() V59() V60() set
bool is non empty non trivial non finite set

Seg 1 is non empty trivial finite 1 -element V67() V68() V69() V70() V71() V72() Element of bool NAT

PI / 2 is V31() real ext-real Element of REAL
- (PI / 2) 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

1r is V31() Element of COMPLEX

the ZeroF of 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

() ^2 is V31() real ext-real Element of REAL
K104((),()) is V31() real ext-real set

() ^2 is V31() real ext-real Element of REAL
K104((),()) is V31() real ext-real set
(() ^2) + (() ^2) is V31() real ext-real Element of REAL
sqrt ((() ^2) + (() ^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

() ^2 is V31() real ext-real Element of REAL
K104((),()) is V31() real ext-real set

() ^2 is V31() real ext-real Element of REAL
K104((),()) is V31() real ext-real set
(() ^2) + (() ^2) is V31() real ext-real Element of REAL
sqrt ((() ^2) + (() ^2)) is V31() real ext-real Element of REAL

K706(cos,0) is V31() real ext-real Element of REAL
K706(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

- 1 is non empty V31() real ext-real non positive negative integer 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

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

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

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

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 non empty V31() real ext-real positive non negative integer finite cardinal rational V67() V68() V69() V70() V71() V72() Element of NAT

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

(MGFC | (Seg 1)) . 1 is 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

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

Seg n is finite n -element V67() V68() V69() V70() V71() V72() Element of bool 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

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
|.().| is V31() real ext-real Element of REAL
Re () is V31() real ext-real Element of REAL
(Re ()) ^2 is V31() real ext-real Element of REAL
K104((Re ()),(Re ())) is V31() real ext-real set
Im () is V31() real ext-real Element of REAL
(Im ()) ^2 is V31() real ext-real Element of REAL
K104((Im ()),(Im ())) is V31() real ext-real set
((Re ()) ^2) + ((Im ()) ^2) is V31() real ext-real Element of REAL
sqrt (((Re ()) ^2) + ((Im ()) ^2)) is V31() real ext-real Element of REAL

qc is V31() real ext-real Element of REAL

(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

ps is V31() right_complementable Element of the carrier of F_Complex

(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

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

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

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

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
|.().| is V31() real ext-real Element of REAL
Re () is V31() real ext-real Element of REAL
(Re ()) ^2 is V31() real ext-real Element of REAL
K104((Re ()),(Re ())) is V31() real ext-real set
Im () is V31() real ext-real Element of REAL
(Im ()) ^2 is V31() real ext-real Element of REAL
K104((Im ()),(Im ())) is V31() real ext-real set
((Re ()) ^2) + ((Im ()) ^2) is V31() real ext-real Element of REAL
sqrt (((Re ()) ^2) + ((Im ()) ^2)) is V31() real ext-real Element of REAL

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
|.().| is V31() real ext-real Element of REAL
Re () is V31() real ext-real Element of REAL
(Re ()) ^2 is V31() real ext-real Element of REAL
K104((Re ()),(Re ())) is V31() real ext-real set
Im () is V31() real ext-real Element of REAL
(Im ()) ^2 is V31() real ext-real Element of REAL
K104((Im ()),(Im ())) is V31() real ext-real set
((Re ()) ^2) + ((Im ()) ^2) is V31() real ext-real Element of REAL
sqrt (((Re ()) ^2) + ((Im ()) ^2)) 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

(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

dom S is finite V67() V68() V69() V70() V71() V72() Element of bool NAT

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

(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),()%> 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),()%>,n) is V31() right_complementable Element of the carrier of F_Complex
p1 is V31() right_complementable Element of the carrier of F_Complex

dom fs is finite V67() V68() V69() V70() V71() V72() Element of bool 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),()%> 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),()%>,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),()%> 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),()%>,n) is V31() right_complementable Element of the carrier of F_Complex

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),()%> 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),()%>,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

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

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

q is V31() right_complementable Element of the carrier of F_Complex

dom fs is finite V67() V68() V69() V70() V71() V72() Element of bool NAT

S . qc is set
fs . qc is set

S . (len S) is set
Sum fs is V31() right_complementable Element of the carrier of F_Complex

(len 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
(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) + () 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),()) is V31() right_complementable Element of the carrier of F_Complex
[(Sum fs),()] is non empty set
{(Sum fs),()} is non empty finite V67() set
{(Sum fs)} is non empty trivial finite 1 -element V67() set
{{(Sum fs),()},{(Sum fs)}} is non empty finite V44() set
the addF of F_Complex . [(Sum fs),()] is set
(Sum fs) + () is V31() Element of COMPLEX

len cMGFC 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

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

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

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

S is 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 + 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 qc is finite V67() V68() V69() V70() V71() V72() Element of bool NAT

(Product qc) * fs is V31() real ext-real Element of REAL

ps is set

rng i is finite V67() V68() V69() Element of bool REAL
{ps} is non empty trivial finite 1 -element set

(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

qi . lc is V31() real ext-real set
qc . lc is V31() real ext-real set

(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

dom q is finite V67() V68() V69() V70() V71() V72() Element of bool NAT

q . qc is V31() real ext-real set
MGFC . qc is V31() real ext-real set

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

dom qc is finite V67() V68() V69()