:: MATRIXC1 semantic presentation

REAL is non zero V33() V162() V163() V164() V168() set
NAT is V162() V163() V164() V165() V166() V167() V168() Element of bool REAL
bool REAL is set
F_Complex is non empty V61() V83() V103() V106() V114() V116() V119() V120() V121() V131() V132() V133() V134() L11()
the U1 of F_Complex is set
NAT is V162() V163() V164() V165() V166() V167() V168() set
bool NAT is set
bool NAT is set
K96(NAT) is V24() set
1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
2 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX is non zero V33() V162() V168() set
the U1 of F_Complex * is functional FinSequence-membered FinSequenceSet of the U1 of F_Complex
COMPLEX * is functional FinSequence-membered FinSequenceSet of COMPLEX
RAT is non zero V33() V162() V163() V164() V165() V168() set
INT is non zero V33() V162() V163() V164() V165() V166() V168() set
[:COMPLEX,COMPLEX:] is complex-yielding set
bool [:COMPLEX,COMPLEX:] is set
[:COMPLEX,REAL:] is complex-yielding V152() V153() set
bool [:COMPLEX,REAL:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is complex-yielding V152() V153() set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is complex-yielding V152() V153() set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is V5( RAT ) complex-yielding V152() V153() set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is V5( RAT ) complex-yielding V152() V153() set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is V5( RAT ) V5( INT ) complex-yielding V152() V153() set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is V5( RAT ) V5( INT ) complex-yielding V152() V153() set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
[:[:NAT,NAT:],NAT:] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
bool [:[:NAT,NAT:],NAT:] is set
0 is Function-like functional zero ordinal natural V52() V107() complex ext-real non positive non negative V161() V162() V163() V164() V165() V166() V167() V168() Element of NAT
0 is Function-like functional zero V162() V163() V164() V165() V166() V167() V168() set
1r is complex Element of COMPLEX
1r *' is complex Element of COMPLEX
compcomplex is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
addcomplex is V1() V4([:COMPLEX,COMPLEX:]) V5( COMPLEX ) Function-like total V18([:COMPLEX,COMPLEX:], COMPLEX ) V25( COMPLEX ) complex-yielding V181( COMPLEX ) V182( COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
diffcomplex is V1() V4([:COMPLEX,COMPLEX:]) V5( COMPLEX ) Function-like total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-yielding Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
multcomplex is V1() V4([:COMPLEX,COMPLEX:]) V5( COMPLEX ) Function-like total V18([:COMPLEX,COMPLEX:], COMPLEX ) V25( COMPLEX ) complex-yielding V181( COMPLEX ) V182( COMPLEX ) Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
multreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like total V18([:REAL,REAL:], REAL ) V25( REAL ) complex-yielding V152() V153() V181( REAL ) V182( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
K177(COMPLEX,addcomplex) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
id COMPLEX is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like one-to-one non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
addcomplex * ((id COMPLEX),compcomplex) is V1() V4([:COMPLEX,COMPLEX:]) V5( COMPLEX ) Function-like total V18([:COMPLEX,COMPLEX:], COMPLEX ) complex-yielding Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
1 / 2 is non zero V52() complex ext-real V161() Element of RAT
<i> is complex Element of COMPLEX
(1 / 2) * <i> is complex Element of COMPLEX
- ((1 / 2) * <i>) is complex Element of COMPLEX
addreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like total V18([:REAL,REAL:], REAL ) V25( REAL ) complex-yielding V152() V153() V181( REAL ) V182( REAL ) Element of bool [:[:REAL,REAL:],REAL:]
0c is Function-like functional zero complex V162() V163() V164() V165() V166() V167() V168() Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices x is set
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg (width x)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular Matrix of len x, width x, COMPLEX
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg (width y)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is ordinal natural complex ext-real non negative set
i is ordinal natural complex ext-real non negative set
[M,i] is set
y * (M,i) is complex Element of COMPLEX
x * (M,i) is complex Element of COMPLEX
(x * (M,i)) *' is complex Element of COMPLEX
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is ordinal natural complex ext-real non negative set
j is ordinal natural complex ext-real non negative set
[i,j] is set
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg (width y)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
y * (i,j) is complex Element of COMPLEX
x * (i,j) is complex Element of COMPLEX
(x * (i,j)) *' is complex Element of COMPLEX
M * (i,j) is complex Element of COMPLEX
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg (width y)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i is ordinal natural complex ext-real non negative set
j is ordinal natural complex ext-real non negative set
[i,j] is set
M * (i,j) is complex Element of COMPLEX
y * (i,j) is complex Element of COMPLEX
(y * (i,j)) *' is complex Element of COMPLEX
(M * (i,j)) *' is complex Element of COMPLEX
((M * (i,j)) *') *' is complex Element of COMPLEX
x is ordinal natural complex ext-real non negative set
y is ordinal natural complex ext-real non negative set
[x,y] is set
M is V1() Function-like FinSequence-like tabular set
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(Seg (len M)),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
x is complex set
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x * y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len (x * y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x * y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field (x * y) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (x * y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field y is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
M is complex Element of the U1 of F_Complex
M * (COMPLEX2Field y) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX (M * (COMPLEX2Field y)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX (M * (COMPLEX2Field y))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (Field2COMPLEX (M * (COMPLEX2Field y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (M * (COMPLEX2Field y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (COMPLEX2Field y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (x * y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (Field2COMPLEX (M * (COMPLEX2Field y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M * (COMPLEX2Field y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is ordinal natural complex ext-real non negative set
y is ordinal natural complex ext-real non negative set
[x,y] is set
M is complex set
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
Indices i is set
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
width i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i),(Seg (width i)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
M * i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(M * i) * (x,y) is complex Element of COMPLEX
i * (x,y) is complex Element of COMPLEX
M * (i * (x,y)) is complex Element of COMPLEX
COMPLEX2Field i is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
j is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
j * (x,y) is complex Element of COMPLEX
(COMPLEX2Field i) * (x,y) is complex Element of the U1 of F_Complex
Indices (COMPLEX2Field i) is set
dom (COMPLEX2Field i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
width (COMPLEX2Field i) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width (COMPLEX2Field i)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (COMPLEX2Field i)),(Seg (width (COMPLEX2Field i))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
COMPLEX2Field (M * i) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
i9 is complex Element of the U1 of F_Complex
i9 * (COMPLEX2Field i) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX (i9 * (COMPLEX2Field i)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX (i9 * (COMPLEX2Field i))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
j9 is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
j9 * (x,y) is complex Element of COMPLEX
(i9 * (COMPLEX2Field i)) * (x,y) is complex Element of the U1 of F_Complex
i9 * ((COMPLEX2Field i) * (x,y)) is complex Element of the U1 of F_Complex
i9 * ((COMPLEX2Field i) * (x,y)) is complex Element of COMPLEX
M * ((COMPLEX2Field i) * (x,y)) is complex Element of COMPLEX
x is complex set
x *' is complex Element of COMPLEX
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x * y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x * y)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x *') * (y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len (x * y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x * y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x * y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x * y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is ordinal natural complex ext-real non negative set
j is ordinal natural complex ext-real non negative set
[i,j] is set
Indices ((x * y)) is set
dom ((x * y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width ((x * y))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ((x * y))),(Seg (width ((x * y)))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg (width y)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (y) is set
dom (y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (y)),(Seg (width (y))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (x * y) is set
dom (x * y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x * y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x * y)),(Seg (width (x * y))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
((x * y)) * (i,j) is complex Element of COMPLEX
(x * y) * (i,j) is complex Element of COMPLEX
((x * y) * (i,j)) *' is complex Element of COMPLEX
M is complex Element of COMPLEX
y * (i,j) is complex Element of COMPLEX
M * (y * (i,j)) is complex Element of COMPLEX
(M * (y * (i,j))) *' is complex Element of COMPLEX
M *' is complex Element of COMPLEX
(y * (i,j)) *' is complex Element of COMPLEX
(M *') * ((y * (i,j)) *') is complex Element of COMPLEX
(y) * (i,j) is complex Element of COMPLEX
(x *') * ((y) * (i,j)) is complex Element of COMPLEX
((x *') * (y)) * (i,j) is complex Element of COMPLEX
len ((x *') * (y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x *') * (y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x + y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len (x + y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x + y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field (x + y) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (x + y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field x is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
COMPLEX2Field y is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
(COMPLEX2Field x) + (COMPLEX2Field y) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX ((COMPLEX2Field x) + (COMPLEX2Field y)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field x) + (COMPLEX2Field y))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field x) + (COMPLEX2Field y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((COMPLEX2Field x) + (COMPLEX2Field y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (COMPLEX2Field x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (x + y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field x) + (COMPLEX2Field y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((COMPLEX2Field x) + (COMPLEX2Field y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is ordinal natural complex ext-real non negative set
y is ordinal natural complex ext-real non negative set
[x,y] is set
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
M + i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(M + i) * (x,y) is complex Element of COMPLEX
M * (x,y) is complex Element of COMPLEX
i * (x,y) is complex Element of COMPLEX
(M * (x,y)) + (i * (x,y)) is complex Element of COMPLEX
COMPLEX2Field (M + i) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
COMPLEX2Field M is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
COMPLEX2Field i is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
(COMPLEX2Field M) + (COMPLEX2Field i) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX ((COMPLEX2Field M) + (COMPLEX2Field i)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M) + (COMPLEX2Field i))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
j is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
j * (x,y) is complex Element of COMPLEX
(COMPLEX2Field M) * (x,y) is complex Element of the U1 of F_Complex
Indices (COMPLEX2Field M) is set
dom (COMPLEX2Field M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
width (COMPLEX2Field M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width (COMPLEX2Field M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (COMPLEX2Field M)),(Seg (width (COMPLEX2Field M))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i9 is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
i9 * (x,y) is complex Element of COMPLEX
(COMPLEX2Field i) * (x,y) is complex Element of the U1 of F_Complex
n3 is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
n3 * (x,y) is complex Element of COMPLEX
(COMPLEX2Field (M + i)) * (x,y) is complex Element of the U1 of F_Complex
((COMPLEX2Field M) * (x,y)) + ((COMPLEX2Field i) * (x,y)) is complex Element of the U1 of F_Complex
((COMPLEX2Field M) * (x,y)) + ((COMPLEX2Field i) * (x,y)) is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x + y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x + y)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) + (y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len (x + y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x + y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x + y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x + y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is ordinal natural complex ext-real non negative set
i is ordinal natural complex ext-real non negative set
[M,i] is set
Indices ((x + y)) is set
dom ((x + y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width ((x + y))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ((x + y))),(Seg (width ((x + y)))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
width (x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices (x) is set
dom (x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x)),(Seg (width (x))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices x is set
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg (width x)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg (width y)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (x + y) is set
dom (x + y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x + y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x + y)),(Seg (width (x + y))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
((x + y)) * (M,i) is complex Element of COMPLEX
(x + y) * (M,i) is complex Element of COMPLEX
((x + y) * (M,i)) *' is complex Element of COMPLEX
x * (M,i) is complex Element of COMPLEX
y * (M,i) is complex Element of COMPLEX
(x * (M,i)) + (y * (M,i)) is complex Element of COMPLEX
((x * (M,i)) + (y * (M,i))) *' is complex Element of COMPLEX
(x * (M,i)) *' is complex Element of COMPLEX
(y * (M,i)) *' is complex Element of COMPLEX
((x * (M,i)) *') + ((y * (M,i)) *') is complex Element of COMPLEX
(x) * (M,i) is complex Element of COMPLEX
((x) * (M,i)) + ((y * (M,i)) *') is complex Element of COMPLEX
(y) * (M,i) is complex Element of COMPLEX
((x) * (M,i)) + ((y) * (M,i)) is complex Element of COMPLEX
((x) + (y)) * (M,i) is complex Element of COMPLEX
width ((x) + (y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x) + (y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
- x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len (- x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (- x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field (- x) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (- x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field x is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
- (COMPLEX2Field x) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX (- (COMPLEX2Field x)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field x))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field x)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (- (COMPLEX2Field x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (COMPLEX2Field x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (- x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field x)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (- (COMPLEX2Field x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is ordinal natural complex ext-real non negative set
y is ordinal natural complex ext-real non negative set
[x,y] is set
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
- M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(- M) * (x,y) is complex Element of COMPLEX
M * (x,y) is complex Element of COMPLEX
- (M * (x,y)) is complex Element of COMPLEX
COMPLEX2Field (- M) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
COMPLEX2Field M is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
- (COMPLEX2Field M) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX (- (COMPLEX2Field M)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX (- (COMPLEX2Field M))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
j is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
j * (x,y) is complex Element of COMPLEX
(COMPLEX2Field M) * (x,y) is complex Element of the U1 of F_Complex
Indices (COMPLEX2Field M) is set
dom (COMPLEX2Field M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
width (COMPLEX2Field M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width (COMPLEX2Field M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (COMPLEX2Field M)),(Seg (width (COMPLEX2Field M))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
i * (x,y) is complex Element of COMPLEX
(- (COMPLEX2Field M)) * (x,y) is complex Element of the U1 of F_Complex
- ((COMPLEX2Field M) * (x,y)) is complex Element of the U1 of F_Complex
- 1 is non zero V52() V107() complex ext-real V161() Element of INT
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(- 1) * x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
- x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width (- x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((- 1) * x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((- 1) * x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is ordinal natural complex ext-real non negative set
M is ordinal natural complex ext-real non negative set
[y,M] is set
Indices ((- 1) * x) is set
dom ((- 1) * x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width ((- 1) * x)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ((- 1) * x)),(Seg (width ((- 1) * x))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices x is set
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg (width x)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
((- 1) * x) * (y,M) is complex Element of COMPLEX
x * (y,M) is complex Element of COMPLEX
(- 1) * (x * (y,M)) is complex Element of COMPLEX
- (x * (y,M)) is complex Element of COMPLEX
(- x) * (y,M) is complex Element of COMPLEX
len (- x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
- x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((- x)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
- (x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(- 1) * x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(((- 1) * x)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
- 1r is complex Element of COMPLEX
(- 1r) *' is complex Element of COMPLEX
((- 1r) *') * (x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(- 1) * (x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x - y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len (x - y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x - y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field (x - y) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (x - y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
COMPLEX2Field x is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
COMPLEX2Field y is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
(COMPLEX2Field x) - (COMPLEX2Field y) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX ((COMPLEX2Field x) - (COMPLEX2Field y)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field x) - (COMPLEX2Field y))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field x) - (COMPLEX2Field y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((COMPLEX2Field x) - (COMPLEX2Field y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
- (COMPLEX2Field y) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
(COMPLEX2Field x) + (- (COMPLEX2Field y)) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width ((COMPLEX2Field x) + (- (COMPLEX2Field y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (COMPLEX2Field x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (x - y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field x) - (COMPLEX2Field y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((COMPLEX2Field x) - (COMPLEX2Field y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((COMPLEX2Field x) + (- (COMPLEX2Field y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (COMPLEX2Field x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is ordinal natural complex ext-real non negative set
y is ordinal natural complex ext-real non negative set
[x,y] is set
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
M - i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(M - i) * (x,y) is complex Element of COMPLEX
M * (x,y) is complex Element of COMPLEX
i * (x,y) is complex Element of COMPLEX
(M * (x,y)) - (i * (x,y)) is complex Element of COMPLEX
Indices i is set
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i),(Seg (width i)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
COMPLEX2Field i is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Indices (COMPLEX2Field i) is set
dom (COMPLEX2Field i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
width (COMPLEX2Field i) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width (COMPLEX2Field i)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (COMPLEX2Field i)),(Seg (width (COMPLEX2Field i))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
COMPLEX2Field M is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
COMPLEX2Field (M - i) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
(COMPLEX2Field M) - (COMPLEX2Field i) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
Field2COMPLEX ((COMPLEX2Field M) - (COMPLEX2Field i)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
COMPLEX2Field (Field2COMPLEX ((COMPLEX2Field M) - (COMPLEX2Field i))) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
i9 is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
i9 * (x,y) is complex Element of COMPLEX
(COMPLEX2Field M) * (x,y) is complex Element of the U1 of F_Complex
Indices (COMPLEX2Field M) is set
dom (COMPLEX2Field M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
width (COMPLEX2Field M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width (COMPLEX2Field M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (COMPLEX2Field M)),(Seg (width (COMPLEX2Field M))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
j is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
j * (x,y) is complex Element of COMPLEX
(COMPLEX2Field i) * (x,y) is complex Element of the U1 of F_Complex
- (i * (x,y)) is complex Element of COMPLEX
- ((COMPLEX2Field i) * (x,y)) is complex Element of the U1 of F_Complex
n3 is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
n3 * (x,y) is complex Element of COMPLEX
(COMPLEX2Field (M - i)) * (x,y) is complex Element of the U1 of F_Complex
- (COMPLEX2Field i) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
(COMPLEX2Field M) + (- (COMPLEX2Field i)) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
((COMPLEX2Field M) + (- (COMPLEX2Field i))) * (x,y) is complex Element of the U1 of F_Complex
(- (COMPLEX2Field i)) * (x,y) is complex Element of the U1 of F_Complex
((COMPLEX2Field M) * (x,y)) + ((- (COMPLEX2Field i)) * (x,y)) is complex Element of the U1 of F_Complex
((COMPLEX2Field M) * (x,y)) + ((- (COMPLEX2Field i)) * (x,y)) is complex Element of COMPLEX
((COMPLEX2Field M) * (x,y)) + (- ((COMPLEX2Field i) * (x,y))) is complex Element of the U1 of F_Complex
((COMPLEX2Field M) * (x,y)) + (- ((COMPLEX2Field i) * (x,y))) is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x - y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x - y)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) - (y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len ((x - y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x - y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x - y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x - y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is ordinal natural complex ext-real non negative set
i is ordinal natural complex ext-real non negative set
[M,i] is set
Indices ((x - y)) is set
dom ((x - y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width ((x - y))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ((x - y))),(Seg (width ((x - y)))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (x) is set
dom (x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x)),(Seg (width (x))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices x is set
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg (width x)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg (width y)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (x - y) is set
dom (x - y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x - y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x - y)),(Seg (width (x - y))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
((x - y)) * (M,i) is complex Element of COMPLEX
(x - y) * (M,i) is complex Element of COMPLEX
((x - y) * (M,i)) *' is complex Element of COMPLEX
x * (M,i) is complex Element of COMPLEX
y * (M,i) is complex Element of COMPLEX
(x * (M,i)) - (y * (M,i)) is complex Element of COMPLEX
((x * (M,i)) - (y * (M,i))) *' is complex Element of COMPLEX
(x * (M,i)) *' is complex Element of COMPLEX
(y * (M,i)) *' is complex Element of COMPLEX
((x * (M,i)) *') - ((y * (M,i)) *') is complex Element of COMPLEX
(x) * (M,i) is complex Element of COMPLEX
((x) * (M,i)) - ((y * (M,i)) *') is complex Element of COMPLEX
(y) * (M,i) is complex Element of COMPLEX
((x) * (M,i)) - ((y) * (M,i)) is complex Element of COMPLEX
((x) - (y)) * (M,i) is complex Element of COMPLEX
width ((x) - (y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x) - (y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() Function-like FinSequence-like set
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
rng M is set
i is set
j is set
M . j is set
i9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x . i9 is complex Element of COMPLEX
<*(x . i9)*> is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len <*(x . i9)*> is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
rng i is functional Element of bool (COMPLEX *)
bool (COMPLEX *) is set
j is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
i9 is ordinal natural complex ext-real non negative set
i . i9 is V1() Function-like set
x . i9 is complex Element of COMPLEX
<*(x . i9)*> is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len <*(x . i9)*> is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg y is V162() V163() V164() V165() V166() V167() Element of bool NAT
j is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular Matrix of len i,1, COMPLEX
width j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i9 is ordinal natural complex ext-real non negative set
i . i9 is V1() Function-like set
x . i9 is complex Element of COMPLEX
<*(x . i9)*> is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is ordinal natural complex ext-real non negative set
y . i is V1() Function-like set
x . i is complex Element of COMPLEX
<*(x . i)*> is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M . i is V1() Function-like set
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
Col (x,1) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (j,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
dom multcomplex is V1() V4( COMPLEX ) V5( COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
rng j is V162() Element of bool COMPLEX
bool COMPLEX is set
rng i is V162() Element of bool COMPLEX
[:(rng j),(rng i):] is complex-yielding set
[:(rng i),(rng j):] is complex-yielding set
dom (multcomplex .: (i,j)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom j is V162() V163() V164() V165() V166() V167() Element of bool NAT
(dom i) /\ (dom j) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (multcomplex .: (j,i)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
i9 is set
M . i9 is complex Element of COMPLEX
j . i9 is complex Element of COMPLEX
i . i9 is complex Element of COMPLEX
multcomplex . ((j . i9),(i . i9)) is complex Element of COMPLEX
multcomplex . ((i . i9),(j . i9)) is complex Element of COMPLEX
(i . i9) * (j . i9) is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is ordinal natural complex ext-real non negative set
M . i is complex Element of COMPLEX
Line (x,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width x) FinSequence-like complex-yielding Element of (width x) -tuples_on COMPLEX
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
((Line (x,i)),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((Line (x,i)),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((Line (x,i)),y) is complex Element of COMPLEX
addcomplex $$ ((Line (x,i)),y) is complex Element of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
j is ordinal natural complex ext-real non negative set
M . j is complex Element of COMPLEX
Line (x,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width x) FinSequence-like complex-yielding Element of (width x) -tuples_on COMPLEX
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
((Line (x,j)),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((Line (x,j)),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((Line (x,j)),y) is complex Element of COMPLEX
addcomplex $$ ((Line (x,j)),y) is complex Element of COMPLEX
i . j is complex Element of COMPLEX
x is complex Element of COMPLEX
multcomplex [;] (x,(id COMPLEX)) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x * y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(multcomplex [;] (x,(id COMPLEX))) * y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x multcomplex is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
x is ordinal natural complex ext-real non negative set
x -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
y is complex Element of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(x) FinSequence-like complex-yielding Element of x -tuples_on COMPLEX
y * M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(x) FinSequence-like complex-yielding Element of x -tuples_on COMPLEX
(M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y * (M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((y * M),i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((y * M),i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex [;] (y,(id COMPLEX)) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
(multcomplex [;] (y,(id COMPLEX))) * (M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(multcomplex [;] (y,(id COMPLEX))) * M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((multcomplex [;] (y,(id COMPLEX))) * M),i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y is complex set
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
y * x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x is complex Element of COMPLEX
(y,x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x * y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((y,x)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x *' is complex Element of COMPLEX
(y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x *') * (y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
dom (x,y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
M is ordinal natural complex ext-real non negative set
(x,y) . M is complex Element of COMPLEX
x . M is complex Element of COMPLEX
y . M is complex Element of COMPLEX
(x . M) * (y . M) is complex Element of COMPLEX
multcomplex . ((x . M),(y . M)) is complex Element of COMPLEX
x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(x) FinSequence-like complex-yielding Element of x -tuples_on COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(x) FinSequence-like complex-yielding Element of x -tuples_on COMPLEX
(y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x is ordinal natural complex ext-real non negative set
x -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
y is ordinal natural complex ext-real non negative set
M is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(x) FinSequence-like complex-yielding Element of x -tuples_on COMPLEX
M . y is complex Element of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(x) FinSequence-like complex-yielding Element of x -tuples_on COMPLEX
(M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(M,i) . y is complex Element of COMPLEX
i . y is complex Element of COMPLEX
(M . y) * (i . y) is complex Element of COMPLEX
j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Seg j is V162() V163() V164() V165() V166() V167() Element of bool NAT
n3 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(j) FinSequence-like complex-yielding Element of j -tuples_on COMPLEX
dom n3 is V162() V163() V164() V165() V166() V167() Element of bool NAT
j9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(j) FinSequence-like complex-yielding Element of j -tuples_on COMPLEX
(j,j9,n3) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(j) FinSequence-like complex-yielding Element of j -tuples_on COMPLEX
multcomplex .: (j9,n3) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
dom (j,j9,n3) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(j,j9,n3) . y is complex Element of COMPLEX
i9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j9 . i9 is complex Element of COMPLEX
(j9 . i9) * 0 is complex Element of COMPLEX
j9 . y is complex Element of COMPLEX
n3 . y is complex Element of COMPLEX
(j9 . y) * (n3 . y) is complex Element of COMPLEX
Seg j is V162() V163() V164() V165() V166() V167() Element of bool NAT
j9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(j) FinSequence-like complex-yielding Element of j -tuples_on COMPLEX
n3 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(j) FinSequence-like complex-yielding Element of j -tuples_on COMPLEX
(j,j9,n3) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40(j) FinSequence-like complex-yielding Element of j -tuples_on COMPLEX
multcomplex .: (j9,n3) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
dom (j,j9,n3) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg j is V162() V163() V164() V165() V166() V167() Element of bool NAT
x is complex Element of COMPLEX
y is complex Element of COMPLEX
y *' is complex Element of COMPLEX
addcomplex . (x,(y *')) is complex Element of COMPLEX
(addcomplex . (x,(y *'))) *' is complex Element of COMPLEX
x *' is complex Element of COMPLEX
addcomplex . ((x *'),y) is complex Element of COMPLEX
x + (y *') is complex Element of COMPLEX
(x + (y *')) *' is complex Element of COMPLEX
(y *') *' is complex Element of COMPLEX
(x *') + ((y *') *') is complex Element of COMPLEX
[:NAT,COMPLEX:] is complex-yielding set
bool [:NAT,COMPLEX:] is set
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
y is set
x . y is complex Element of COMPLEX
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like total V18( NAT , COMPLEX ) complex-yielding Element of bool [:NAT,COMPLEX:]
y is V1() V4( NAT ) V5( COMPLEX ) Function-like total V18( NAT , COMPLEX ) complex-yielding Element of bool [:NAT,COMPLEX:]
M is ordinal natural complex ext-real non negative set
y . M is complex Element of COMPLEX
x . M is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
addcomplex $$ (x *') is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
(addcomplex $$ x) *' is complex Element of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x *') . 1 is complex Element of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like total V18( NAT , COMPLEX ) complex-yielding Element of bool [:NAT,COMPLEX:]
y . 1 is complex Element of COMPLEX
y . (len (x *')) is complex Element of COMPLEX
Seg (len (x *')) is V162() V163() V164() V165() V166() V167() Element of bool NAT
M is ordinal natural complex ext-real non negative set
y . M is complex Element of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
M *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (M *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is V1() V4( NAT ) V5( COMPLEX ) Function-like total V18( NAT , COMPLEX ) complex-yielding Element of bool [:NAT,COMPLEX:]
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i . 1 is complex Element of COMPLEX
(M *') . 1 is complex Element of COMPLEX
j is ordinal natural complex ext-real non negative set
j + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M . (j + 1) is complex Element of COMPLEX
M . j is complex Element of COMPLEX
(x *') . (j + 1) is complex Element of COMPLEX
addcomplex . ((M . j),((x *') . (j + 1))) is complex Element of COMPLEX
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y . (j + 1) is complex Element of COMPLEX
y . j is complex Element of COMPLEX
addcomplex . ((y . j),((x *') . (j + 1))) is complex Element of COMPLEX
j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M *') . (j + 1) is complex Element of COMPLEX
(M *') . j is complex Element of COMPLEX
x . (j + 1) is complex Element of COMPLEX
addcomplex . (((M *') . j),(x . (j + 1))) is complex Element of COMPLEX
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M . (j + 1) is complex Element of COMPLEX
(M . (j + 1)) *' is complex Element of COMPLEX
M . j is complex Element of COMPLEX
(x *') . (j + 1) is complex Element of COMPLEX
addcomplex . ((M . j),((x *') . (j + 1))) is complex Element of COMPLEX
(addcomplex . ((M . j),((x *') . (j + 1)))) *' is complex Element of COMPLEX
(x . (j + 1)) *' is complex Element of COMPLEX
addcomplex . ((M . j),((x . (j + 1)) *')) is complex Element of COMPLEX
(addcomplex . ((M . j),((x . (j + 1)) *'))) *' is complex Element of COMPLEX
(M . j) *' is complex Element of COMPLEX
addcomplex . (((M . j) *'),(x . (j + 1))) is complex Element of COMPLEX
j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i . (j + 1) is complex Element of COMPLEX
i . j is complex Element of COMPLEX
x . (j + 1) is complex Element of COMPLEX
addcomplex . ((i . j),(x . (j + 1))) is complex Element of COMPLEX
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M *') . (j + 1) is complex Element of COMPLEX
(M *') . j is complex Element of COMPLEX
(addcomplex $$ (x *')) *' is complex Element of COMPLEX
(M *') . (len x) is complex Element of COMPLEX
(M *') . (len (x *')) is complex Element of COMPLEX
M . (len (x *')) is complex Element of COMPLEX
(M . (len (x *'))) *' is complex Element of COMPLEX
i . (len x) is complex Element of COMPLEX
x . 1 is complex Element of COMPLEX
(x . 1) *' is complex Element of COMPLEX
((x . 1) *') *' is complex Element of COMPLEX
((x *') . 1) *' is complex Element of COMPLEX
M . 1 is complex Element of COMPLEX
(M . 1) *' is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x *') is complex Element of COMPLEX
addcomplex $$ (x *') is complex Element of COMPLEX
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
(Sum x) *' is complex Element of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,(y *')) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y,(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len (x *')) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (y *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len (y *')) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (x,(y *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j9 is ordinal natural complex ext-real non negative set
len ((x,(y *')) *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((x,(y *')) *') . j9 is complex Element of COMPLEX
(x,(y *')) . j9 is complex Element of COMPLEX
((x,(y *')) . j9) *' is complex Element of COMPLEX
i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
i9 . j9 is complex Element of COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len (y *')) FinSequence-like complex-yielding Element of (len (y *')) -tuples_on COMPLEX
j . j9 is complex Element of COMPLEX
(i9 . j9) * (j . j9) is complex Element of COMPLEX
((i9 . j9) * (j . j9)) *' is complex Element of COMPLEX
x . j9 is complex Element of COMPLEX
(x . j9) *' is complex Element of COMPLEX
(y *') . j9 is complex Element of COMPLEX
((y *') . j9) *' is complex Element of COMPLEX
((x . j9) *') * (((y *') . j9) *') is complex Element of COMPLEX
(y *') *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((y *') *') . j9 is complex Element of COMPLEX
((x . j9) *') * (((y *') *') . j9) is complex Element of COMPLEX
y . j9 is complex Element of COMPLEX
((x . j9) *') * (y . j9) is complex Element of COMPLEX
(x *') . j9 is complex Element of COMPLEX
((x *') . j9) * (y . j9) is complex Element of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len (x *')) FinSequence-like complex-yielding Element of (len (x *')) -tuples_on COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len y) FinSequence-like complex-yielding Element of (len y) -tuples_on COMPLEX
(M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (M,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(M,i) . j9 is complex Element of COMPLEX
(y,(x *')) . j9 is complex Element of COMPLEX
len (y,(x *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M is complex Element of COMPLEX
M * y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,(M * y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(M * y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M * (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len y) FinSequence-like complex-yielding Element of (len y) -tuples_on COMPLEX
(i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M * (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M is complex Element of COMPLEX
M * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((M * x),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((M * x),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M * (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len y) FinSequence-like complex-yielding Element of (len y) -tuples_on COMPLEX
(i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M * (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,y) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((x *'),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((x *'),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((x,y) *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x,y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is ordinal natural complex ext-real non negative set
((x,y) *') . M is complex Element of COMPLEX
((x *'),(y *')) . M is complex Element of COMPLEX
(x *') *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y,((x *') *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,((x *') *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y,((x *') *')) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((y,((x *') *')) *') . M is complex Element of COMPLEX
len (y *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x *'),(y *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is complex Element of COMPLEX
multcomplex [;] (x,(id COMPLEX)) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
y is complex Element of COMPLEX
(multcomplex [;] (x,(id COMPLEX))) . y is complex Element of COMPLEX
x * y is complex Element of COMPLEX
(id COMPLEX) . y is complex Element of COMPLEX
multcomplex . (x,((id COMPLEX) . y)) is complex Element of COMPLEX
multcomplex . (x,y) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
y is complex Element of COMPLEX
y * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (y * x) is complex Element of COMPLEX
addcomplex $$ (y * x) is complex Element of COMPLEX
y * (Sum x) is complex Element of COMPLEX
multcomplex [;] (y,(id COMPLEX)) is V1() V4( COMPLEX ) V5( COMPLEX ) Function-like non zero total V18( COMPLEX , COMPLEX ) complex-yielding Element of bool [:COMPLEX,COMPLEX:]
(multcomplex [;] (y,(id COMPLEX))) * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
addcomplex $$ ((multcomplex [;] (y,(id COMPLEX))) * x) is complex Element of COMPLEX
(multcomplex [;] (y,(id COMPLEX))) . (addcomplex $$ x) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
rng x is V162() V163() V164() Element of bool REAL
x is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
addreal $$ x is V52() complex ext-real Element of REAL
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
[:NAT,REAL:] is complex-yielding V152() V153() set
bool [:NAT,REAL:] is set
x . 1 is V52() complex ext-real Element of REAL
M is V1() V4( NAT ) V5( REAL ) Function-like total V18( NAT , REAL ) complex-yielding V152() V153() Element of bool [:NAT,REAL:]
M . 1 is V52() complex ext-real Element of REAL
M . (len x) is V52() complex ext-real Element of REAL
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is ordinal natural complex ext-real non negative set
M . i is V52() complex ext-real Element of REAL
i is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
(i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (i) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is V1() V4( NAT ) V5( COMPLEX ) Function-like total V18( NAT , COMPLEX ) complex-yielding Element of bool [:NAT,COMPLEX:]
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(i) . (len y) is complex Element of COMPLEX
j . (len y) is complex Element of COMPLEX
i9 is ordinal natural complex ext-real non negative set
i9 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i . (i9 + 1) is V52() complex ext-real Element of REAL
i . i9 is V52() complex ext-real Element of REAL
x . (i9 + 1) is V52() complex ext-real Element of REAL
addreal . ((i . i9),(x . (i9 + 1))) is V52() complex ext-real Element of REAL
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M . (i9 + 1) is V52() complex ext-real Element of REAL
M . i9 is V52() complex ext-real Element of REAL
addreal . ((M . i9),(x . (i9 + 1))) is V52() complex ext-real Element of REAL
i9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i9 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j . (i9 + 1) is complex Element of COMPLEX
j . i9 is complex Element of COMPLEX
y . (i9 + 1) is complex Element of COMPLEX
addcomplex . ((j . i9),(y . (i9 + 1))) is complex Element of COMPLEX
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(i) . i9 is complex Element of COMPLEX
i . i9 is V52() complex ext-real Element of REAL
x . (i9 + 1) is V52() complex ext-real Element of REAL
addreal . ((i . i9),(x . (i9 + 1))) is V52() complex ext-real Element of REAL
(i) . (i9 + 1) is complex Element of COMPLEX
j . 1 is complex Element of COMPLEX
(i) . 1 is complex Element of COMPLEX
x is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Sum x is V52() complex ext-real Element of REAL
addreal $$ x is V52() complex ext-real Element of REAL
Sum y is complex Element of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x - y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385(y) is V1() Function-like complex-yielding set
- 1 is non zero complex set
(- 1) * y is V1() Function-like set
K356(x,K385(y)) is V1() Function-like set
Sum (x - y) is complex Element of COMPLEX
addcomplex $$ (x - y) is complex Element of COMPLEX
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
Sum y is complex Element of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
(Sum x) - (Sum y) is complex Element of COMPLEX
(len y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
diffcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
addcomplex $$ (diffcomplex .: (x,y)) is complex Element of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
addcomplex $$ i is complex Element of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len y) FinSequence-like complex-yielding Element of (len y) -tuples_on COMPLEX
addcomplex $$ M is complex Element of COMPLEX
diffcomplex . ((addcomplex $$ i),(addcomplex $$ M)) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x - y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385(y) is V1() Function-like complex-yielding set
- 1 is non zero complex set
(- 1) * y is V1() Function-like set
K356(x,K385(y)) is V1() Function-like set
((x - y),M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((x - y),M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,M) - (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((y,M)) is V1() Function-like complex-yielding set
(- 1) * (y,M) is V1() Function-like set
K356((x,M),K385((y,M))) is V1() Function-like set
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
dom ((x - y),M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
i - j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
K385(j) is V1() Function-like complex-yielding set
(- 1) * j is V1() Function-like set
K356(i,K385(j)) is V1() Function-like set
i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
((len x),(i - j),i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: ((i - j),i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((len x),(i - j),i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),(i - j),i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((len x),i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),j,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (j,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),i,i9) - ((len x),j,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
K385(((len x),j,i9)) is V1() Function-like complex-yielding set
(- 1) * ((len x),j,i9) is V1() Function-like set
K356(((len x),i,i9),K385(((len x),j,i9))) is V1() Function-like set
len (((len x),i,i9) - ((len x),j,i9)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (((len x),i,i9) - ((len x),j,i9))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (((len x),i,i9) - ((len x),j,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (x,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),i,i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (y,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),j,i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),j,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
j9 is ordinal natural complex ext-real non negative set
((x - y),M) . j9 is complex Element of COMPLEX
((x,M) - (y,M)) . j9 is complex Element of COMPLEX
x . j9 is complex Element of COMPLEX
y . j9 is complex Element of COMPLEX
(x - y) . j9 is complex Element of COMPLEX
M . j9 is complex Element of COMPLEX
len (i - j) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom (i - j) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(x . j9) - (y . j9) is complex Element of COMPLEX
((x - y) . j9) * (M . j9) is complex Element of COMPLEX
(x . j9) * (M . j9) is complex Element of COMPLEX
(y . j9) * (M . j9) is complex Element of COMPLEX
((x . j9) * (M . j9)) - ((y . j9) * (M . j9)) is complex Element of COMPLEX
(x,M) . j9 is complex Element of COMPLEX
((x,M) . j9) - ((y . j9) * (M . j9)) is complex Element of COMPLEX
(y,M) . j9 is complex Element of COMPLEX
((x,M) . j9) - ((y,M) . j9) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y - M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385(M) is V1() Function-like complex-yielding set
- 1 is non zero complex set
(- 1) * M is V1() Function-like set
K356(y,K385(M)) is V1() Function-like set
(x,(y - M)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(y - M)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,y) - (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((x,M)) is V1() Function-like complex-yielding set
(- 1) * (x,M) is V1() Function-like set
K356((x,y),K385((x,M))) is V1() Function-like set
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
dom (x,(y - M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j - i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
K385(i9) is V1() Function-like complex-yielding set
(- 1) * i9 is V1() Function-like set
K356(j,K385(i9)) is V1() Function-like set
((len x),i,(j - i9)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,(j - i9)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((len x),i,(j - i9)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,(j - i9))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((len x),i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),i,j) - ((len x),i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
K385(((len x),i,i9)) is V1() Function-like complex-yielding set
(- 1) * ((len x),i,i9) is V1() Function-like set
K356(((len x),i,j),K385(((len x),i,i9))) is V1() Function-like set
len (((len x),i,j) - ((len x),i,i9)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (((len x),i,j) - ((len x),i,i9))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (((len x),i,j) - ((len x),i,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (x,y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),i,j) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,j)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (x,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),i,i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
j9 is ordinal natural complex ext-real non negative set
(x,(y - M)) . j9 is complex Element of COMPLEX
((x,y) - (x,M)) . j9 is complex Element of COMPLEX
y . j9 is complex Element of COMPLEX
M . j9 is complex Element of COMPLEX
(y - M) . j9 is complex Element of COMPLEX
x . j9 is complex Element of COMPLEX
len (j - i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom (j - i9) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(y . j9) - (M . j9) is complex Element of COMPLEX
(x . j9) * ((y - M) . j9) is complex Element of COMPLEX
(x . j9) * (y . j9) is complex Element of COMPLEX
(x . j9) * (M . j9) is complex Element of COMPLEX
((x . j9) * (y . j9)) - ((x . j9) * (M . j9)) is complex Element of COMPLEX
(x,y) . j9 is complex Element of COMPLEX
((x,y) . j9) - ((x . j9) * (M . j9)) is complex Element of COMPLEX
(x,M) . j9 is complex Element of COMPLEX
((x,y) . j9) - ((x,M) . j9) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y + M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,(y + M)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(y + M)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,y) + (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
dom (x,(y + M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j + i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
((len x),i,(j + i9)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,(j + i9)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((len x),i,(j + i9)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,(j + i9))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((len x),i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),i,j) + ((len x),i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
len (((len x),i,j) + ((len x),i,i9)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (((len x),i,j) + ((len x),i,i9))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (((len x),i,j) + ((len x),i,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (x,y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),i,j) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,j)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (x,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),i,i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
j9 is ordinal natural complex ext-real non negative set
(x,(y + M)) . j9 is complex Element of COMPLEX
((x,y) + (x,M)) . j9 is complex Element of COMPLEX
y . j9 is complex Element of COMPLEX
M . j9 is complex Element of COMPLEX
(y + M) . j9 is complex Element of COMPLEX
x . j9 is complex Element of COMPLEX
len (j + i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom (j + i9) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(y . j9) + (M . j9) is complex Element of COMPLEX
(x . j9) * ((y + M) . j9) is complex Element of COMPLEX
(x . j9) * (y . j9) is complex Element of COMPLEX
(x . j9) * (M . j9) is complex Element of COMPLEX
((x . j9) * (y . j9)) + ((x . j9) * (M . j9)) is complex Element of COMPLEX
(x,y) . j9 is complex Element of COMPLEX
((x,y) . j9) + ((x . j9) * (M . j9)) is complex Element of COMPLEX
(x,M) . j9 is complex Element of COMPLEX
((x,y) . j9) + ((x,M) . j9) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x + y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((x + y),M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((x + y),M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,M) + (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
dom ((x + y),M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
i + j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
((len x),(i + j),i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: ((i + j),i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((len x),(i + j),i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),(i + j),i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((len x),i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (i,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),j,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
multcomplex .: (j,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((len x),i,i9) + ((len x),j,i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
len (((len x),i,i9) + ((len x),j,i9)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (((len x),i,i9) + ((len x),j,i9))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (((len x),i,i9) + ((len x),j,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (x,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),i,i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),i,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (y,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((len x),j,i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((len x),j,i9)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
j9 is ordinal natural complex ext-real non negative set
((x + y),M) . j9 is complex Element of COMPLEX
((x,M) + (y,M)) . j9 is complex Element of COMPLEX
x . j9 is complex Element of COMPLEX
y . j9 is complex Element of COMPLEX
(x + y) . j9 is complex Element of COMPLEX
M . j9 is complex Element of COMPLEX
len (i + j) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom (i + j) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(x . j9) + (y . j9) is complex Element of COMPLEX
((x + y) . j9) * (M . j9) is complex Element of COMPLEX
(x . j9) * (M . j9) is complex Element of COMPLEX
(y . j9) * (M . j9) is complex Element of COMPLEX
((x . j9) * (M . j9)) + ((y . j9) * (M . j9)) is complex Element of COMPLEX
(x,M) . j9 is complex Element of COMPLEX
((x,M) . j9) + ((y . j9) * (M . j9)) is complex Element of COMPLEX
(y,M) . j9 is complex Element of COMPLEX
((x,M) . j9) + ((y,M) . j9) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x + y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x + y) is complex Element of COMPLEX
addcomplex $$ (x + y) is complex Element of COMPLEX
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
Sum y is complex Element of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
(Sum x) + (Sum y) is complex Element of COMPLEX
(len y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
addcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
addcomplex $$ (addcomplex .: (x,y)) is complex Element of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
addcomplex $$ i is complex Element of COMPLEX
M is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len y) FinSequence-like complex-yielding Element of (len y) -tuples_on COMPLEX
addcomplex $$ M is complex Element of COMPLEX
addcomplex . ((addcomplex $$ i),(addcomplex $$ M)) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
i is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
multreal .: (M,i) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x . j is complex Element of COMPLEX
y . j is complex Element of COMPLEX
multcomplex . ((x . j),(y . j)) is complex Element of COMPLEX
M . j is V52() complex ext-real Element of REAL
i . j is V52() complex ext-real Element of REAL
multreal . ((M . j),(i . j)) is V52() complex ext-real Element of REAL
(x . j) * (y . j) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
mlt (x,y) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
multreal .: (x,y) is set
((mlt (x,y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((x),(y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((x),(y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
|(x,y)| is complex Element of COMPLEX
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x,(y *')) is complex Element of COMPLEX
addcomplex $$ (x,(y *')) is complex Element of COMPLEX
Im y is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
len (Im y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
- (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
- 1 is non zero complex set
(- 1) * (y *') is V1() Function-like set
- (- (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(- 1) * (- (y *')) is V1() Function-like set
(- 1) * (- 1) is non zero V52() V107() complex ext-real V161() Element of INT
((- 1) * (- 1)) * (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
1 * (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x + (x *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x + (x *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x *') + x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((x *') + x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
- x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(- 1) * x is V1() Function-like set
- (- x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(- 1) * (- x) is V1() Function-like set
((- 1) * (- 1)) * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
1 * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Im x is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
((Im x)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((Im x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((Im y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Re y is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
((Re y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Re x is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
((Re x)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
<i> * ((Im x)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (<i> * ((Im x))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((Re x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (Im x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
mlt ((Im x),(Im y)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
multreal .: ((Im x),(Im y)) is set
(((Im x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Im x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (Re y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
mlt ((Im x),(Re y)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
multreal .: ((Im x),(Re y)) is set
(((Im x)),((Re y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Im x)),((Re y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (Re x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
mlt ((Re x),(Re y)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
multreal .: ((Re x),(Re y)) is set
(((Re x)),((Re y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Re x)),((Re y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
mlt ((Re x),(Im y)) is V1() V4( NAT ) V5( REAL ) Function-like FinSequence-like complex-yielding V152() V153() FinSequence of REAL
multreal .: ((Re x),(Im y)) is set
(((Re x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Re x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x - (x *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((x *')) is V1() Function-like complex-yielding set
(- 1) * (x *') is V1() Function-like set
K356(x,K385((x *'))) is V1() Function-like set
(- ((1 / 2) * <i>)) * (x - (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
<i> * (- ((1 / 2) * <i>)) is complex Element of COMPLEX
(<i> * (- ((1 / 2) * <i>))) * (x - (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (x - (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y - (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((y *')) is V1() Function-like complex-yielding set
K356(y,K385((y *'))) is V1() Function-like set
(- ((1 / 2) * <i>)) * (y - (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
<i> * ((Im y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(<i> * (- ((1 / 2) * <i>))) * (y - (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (y - (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (x + (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y + (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (y + (y *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x - (x *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((Re x)) + (<i> * ((Im x))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x + (x *')) + (x - (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * ((x + (x *')) + (x - (x *'))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x + ((x *') + x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x + ((x *') + x)) - (x *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K356((x + ((x *') + x)),K385((x *'))) is V1() Function-like set
(1 / 2) * ((x + ((x *') + x)) - (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x + (x *')) - (x *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K356((x + (x *')),K385((x *'))) is V1() Function-like set
x + ((x + (x *')) - (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (x + ((x + (x *')) - (x *'))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x *') - (x *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K356((x *'),K385((x *'))) is V1() Function-like set
x + ((x *') - (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x + (x + ((x *') - (x *'))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (x + (x + ((x *') - (x *')))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
0c (len (x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding Element of COMPLEX (len (x *'))
COMPLEX (len (x *')) is functional FinSequence-membered FinSequenceSet of COMPLEX
x + (0c (len (x *'))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x + (x + (0c (len (x *')))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (x + (x + (0c (len (x *'))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
0c (len x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding Element of COMPLEX (len x)
COMPLEX (len x) is functional FinSequence-membered FinSequenceSet of COMPLEX
x + (0c (len x)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x + (x + (0c (len x))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (x + (x + (0c (len x)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x + x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (x + x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((1 / 2) * x) + ((1 / 2) * x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) + (1 / 2) is V52() complex ext-real V161() Element of RAT
((1 / 2) + (1 / 2)) * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (y + (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (y - (y *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((Re y)) - (<i> * ((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((<i> * ((Im y)))) is V1() Function-like complex-yielding set
(- 1) * (<i> * ((Im y))) is V1() Function-like set
K356(((Re y)),K385((<i> * ((Im y))))) is V1() Function-like set
(y + (y *')) - (y - (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((y - (y *'))) is V1() Function-like complex-yielding set
(- 1) * (y - (y *')) is V1() Function-like set
K356((y + (y *')),K385((y - (y *')))) is V1() Function-like set
(1 / 2) * ((y + (y *')) - (y - (y *'))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y *') + y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((y *') + y) - y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385(y) is V1() Function-like complex-yielding set
(- 1) * y is V1() Function-like set
K356(((y *') + y),K385(y)) is V1() Function-like set
(((y *') + y) - y) + (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * ((((y *') + y) - y) + (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y - y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K356(y,K385(y)) is V1() Function-like set
(y *') + (y - y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((y *') + (y - y)) + (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (((y *') + (y - y)) + (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
0c (len y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding Element of COMPLEX (len y)
COMPLEX (len y) is functional FinSequence-membered FinSequenceSet of COMPLEX
(y *') + (0c (len y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((y *') + (0c (len y))) + (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (((y *') + (0c (len y))) + (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y *') + (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * ((y *') + (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(1 / 2) * (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((1 / 2) * (y *')) + ((1 / 2) * (y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((1 / 2) + (1 / 2)) * (y *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((Re y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (((Re x)),((Re y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (<i> * ((Im y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((Im y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(((Re x)),(<i> * ((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Re x)),(<i> * ((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (((Re x)),(<i> * ((Im y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((((Re x)),(<i> * ((Im y))))) is V1() Function-like complex-yielding set
(- 1) * (((Re x)),(<i> * ((Im y)))) is V1() Function-like set
K356((((Re x)),((Re y))),K385((((Re x)),(<i> * ((Im y)))))) is V1() Function-like set
len ((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (((Im x)),((Re y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(((Im x)),(<i> * ((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Im x)),(<i> * ((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (((Im x)),(<i> * ((Im y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (((Im x)),((Im y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
<i> * (((Re x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (<i> * (((Re x)),((Im y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (((Re x)),((Im y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
<i> * (((Im x)),((Re y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (<i> * (((Im x)),((Re y)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(((Re x)),((Re y))) - (<i> * (((Re x)),((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((<i> * (((Re x)),((Im y))))) is V1() Function-like complex-yielding set
(- 1) * (<i> * (((Re x)),((Im y)))) is V1() Function-like set
K356((((Re x)),((Re y))),K385((<i> * (((Re x)),((Im y)))))) is V1() Function-like set
len ((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y))))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
|((Re x),(Re y))| is V52() complex ext-real Element of REAL
Sum (mlt ((Re x),(Re y))) is V52() complex ext-real Element of REAL
addreal $$ (mlt ((Re x),(Re y))) is V52() complex ext-real Element of REAL
|((Re x),(Im y))| is V52() complex ext-real Element of REAL
Sum (mlt ((Re x),(Im y))) is V52() complex ext-real Element of REAL
addreal $$ (mlt ((Re x),(Im y))) is V52() complex ext-real Element of REAL
<i> * |((Re x),(Im y))| is complex Element of COMPLEX
|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|) is complex Element of COMPLEX
|((Im x),(Re y))| is V52() complex ext-real Element of REAL
Sum (mlt ((Im x),(Re y))) is V52() complex ext-real Element of REAL
addreal $$ (mlt ((Im x),(Re y))) is V52() complex ext-real Element of REAL
<i> * |((Im x),(Re y))| is complex Element of COMPLEX
(|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|) is complex Element of COMPLEX
|((Im x),(Im y))| is V52() complex ext-real Element of REAL
Sum (mlt ((Im x),(Im y))) is V52() complex ext-real Element of REAL
addreal $$ (mlt ((Im x),(Im y))) is V52() complex ext-real Element of REAL
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is complex Element of COMPLEX
(Sum (mlt ((Re x),(Re y)))) - (<i> * |((Re x),(Im y))|) is complex Element of COMPLEX
((Sum (mlt ((Re x),(Re y)))) - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|) is complex Element of COMPLEX
(((Sum (mlt ((Re x),(Re y)))) - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is complex Element of COMPLEX
<i> * (Sum (mlt ((Re x),(Im y)))) is complex Element of COMPLEX
(Sum (mlt ((Re x),(Re y)))) - (<i> * (Sum (mlt ((Re x),(Im y))))) is complex Element of COMPLEX
((Sum (mlt ((Re x),(Re y)))) - (<i> * (Sum (mlt ((Re x),(Im y)))))) + (<i> * |((Im x),(Re y))|) is complex Element of COMPLEX
(((Sum (mlt ((Re x),(Re y)))) - (<i> * (Sum (mlt ((Re x),(Im y)))))) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is complex Element of COMPLEX
<i> * (Sum (mlt ((Im x),(Re y)))) is complex Element of COMPLEX
((Sum (mlt ((Re x),(Re y)))) - (<i> * (Sum (mlt ((Re x),(Im y)))))) + (<i> * (Sum (mlt ((Im x),(Re y))))) is complex Element of COMPLEX
(((Sum (mlt ((Re x),(Re y)))) - (<i> * (Sum (mlt ((Re x),(Im y)))))) + (<i> * (Sum (mlt ((Im x),(Re y)))))) + |((Im x),(Im y))| is complex Element of COMPLEX
Sum (((Re x)),((Re y))) is complex Element of COMPLEX
addcomplex $$ (((Re x)),((Re y))) is complex Element of COMPLEX
Sum (((Re x)),((Im y))) is complex Element of COMPLEX
addcomplex $$ (((Re x)),((Im y))) is complex Element of COMPLEX
<i> * (Sum (((Re x)),((Im y)))) is complex Element of COMPLEX
(Sum (((Re x)),((Re y)))) - (<i> * (Sum (((Re x)),((Im y))))) is complex Element of COMPLEX
Sum (((Im x)),((Re y))) is complex Element of COMPLEX
addcomplex $$ (((Im x)),((Re y))) is complex Element of COMPLEX
<i> * (Sum (((Im x)),((Re y)))) is complex Element of COMPLEX
((Sum (((Re x)),((Re y)))) - (<i> * (Sum (((Re x)),((Im y)))))) + (<i> * (Sum (((Im x)),((Re y))))) is complex Element of COMPLEX
(((Sum (((Re x)),((Re y)))) - (<i> * (Sum (((Re x)),((Im y)))))) + (<i> * (Sum (((Im x)),((Re y)))))) + (Sum (mlt ((Im x),(Im y)))) is complex Element of COMPLEX
Sum (<i> * (((Re x)),((Im y)))) is complex Element of COMPLEX
addcomplex $$ (<i> * (((Re x)),((Im y)))) is complex Element of COMPLEX
(Sum (((Re x)),((Re y)))) - (Sum (<i> * (((Re x)),((Im y))))) is complex Element of COMPLEX
((Sum (((Re x)),((Re y)))) - (Sum (<i> * (((Re x)),((Im y)))))) + (<i> * (Sum (((Im x)),((Re y))))) is complex Element of COMPLEX
Sum (((Im x)),((Im y))) is complex Element of COMPLEX
addcomplex $$ (((Im x)),((Im y))) is complex Element of COMPLEX
(((Sum (((Re x)),((Re y)))) - (Sum (<i> * (((Re x)),((Im y)))))) + (<i> * (Sum (((Im x)),((Re y)))))) + (Sum (((Im x)),((Im y)))) is complex Element of COMPLEX
Sum (<i> * (((Im x)),((Re y)))) is complex Element of COMPLEX
addcomplex $$ (<i> * (((Im x)),((Re y)))) is complex Element of COMPLEX
((Sum (((Re x)),((Re y)))) - (Sum (<i> * (((Re x)),((Im y)))))) + (Sum (<i> * (((Im x)),((Re y))))) is complex Element of COMPLEX
(((Sum (((Re x)),((Re y)))) - (Sum (<i> * (((Re x)),((Im y)))))) + (Sum (<i> * (((Im x)),((Re y)))))) + (Sum (((Im x)),((Im y)))) is complex Element of COMPLEX
Sum ((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) is complex Element of COMPLEX
addcomplex $$ ((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) is complex Element of COMPLEX
(Sum ((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y)))))) + (Sum (<i> * (((Im x)),((Re y))))) is complex Element of COMPLEX
((Sum ((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y)))))) + (Sum (<i> * (((Im x)),((Re y)))))) + (Sum (((Im x)),((Im y)))) is complex Element of COMPLEX
Sum (((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y))))) is complex Element of COMPLEX
addcomplex $$ (((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y))))) is complex Element of COMPLEX
(Sum (((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y)))))) + (Sum (((Im x)),((Im y)))) is complex Element of COMPLEX
(((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y))))) + (((Im x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y))))) + (((Im x)),((Im y)))) is complex Element of COMPLEX
addcomplex $$ ((((((Re x)),((Re y))) - (<i> * (((Re x)),((Im y))))) + (<i> * (((Im x)),((Re y))))) + (((Im x)),((Im y)))) is complex Element of COMPLEX
((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * (((Im x)),((Re y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * (((Im x)),((Re y))))) + (((Im x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * (((Im x)),((Re y))))) + (((Im x)),((Im y)))) is complex Element of COMPLEX
addcomplex $$ ((((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * (((Im x)),((Re y))))) + (((Im x)),((Im y)))) is complex Element of COMPLEX
- (((Im x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(- 1) * (((Im x)),((Im y))) is V1() Function-like set
- (- (((Im x)),((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(- 1) * (- (((Im x)),((Im y)))) is V1() Function-like set
(<i> * (((Im x)),((Re y)))) + (- (- (((Im x)),((Im y))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) + (- (- (((Im x)),((Im y)))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) + (- (- (((Im x)),((Im y))))))) is complex Element of COMPLEX
addcomplex $$ (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) + (- (- (((Im x)),((Im y))))))) is complex Element of COMPLEX
<i> * <i> is complex Element of COMPLEX
(<i> * <i>) * (((Im x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(<i> * (((Im x)),((Re y)))) - ((<i> * <i>) * (((Im x)),((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385(((<i> * <i>) * (((Im x)),((Im y))))) is V1() Function-like complex-yielding set
(- 1) * ((<i> * <i>) * (((Im x)),((Im y)))) is V1() Function-like set
K356((<i> * (((Im x)),((Re y)))),K385(((<i> * <i>) * (((Im x)),((Im y)))))) is V1() Function-like set
((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - ((<i> * <i>) * (((Im x)),((Im y))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - ((<i> * <i>) * (((Im x)),((Im y)))))) is complex Element of COMPLEX
addcomplex $$ (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - ((<i> * <i>) * (((Im x)),((Im y)))))) is complex Element of COMPLEX
<i> * (((Im x)),((Im y))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
<i> * (<i> * (((Im x)),((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(<i> * (((Im x)),((Re y)))) - (<i> * (<i> * (((Im x)),((Im y))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((<i> * (<i> * (((Im x)),((Im y)))))) is V1() Function-like complex-yielding set
(- 1) * (<i> * (<i> * (((Im x)),((Im y))))) is V1() Function-like set
K356((<i> * (((Im x)),((Re y)))),K385((<i> * (<i> * (((Im x)),((Im y))))))) is V1() Function-like set
((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - (<i> * (<i> * (((Im x)),((Im y)))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - (<i> * (<i> * (((Im x)),((Im y))))))) is complex Element of COMPLEX
addcomplex $$ (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - (<i> * (<i> * (((Im x)),((Im y))))))) is complex Element of COMPLEX
<i> * (((Im x)),(<i> * ((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(<i> * (((Im x)),((Re y)))) - (<i> * (((Im x)),(<i> * ((Im y))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((<i> * (((Im x)),(<i> * ((Im y)))))) is V1() Function-like complex-yielding set
(- 1) * (<i> * (((Im x)),(<i> * ((Im y))))) is V1() Function-like set
K356((<i> * (((Im x)),((Re y)))),K385((<i> * (((Im x)),(<i> * ((Im y))))))) is V1() Function-like set
((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - (<i> * (((Im x)),(<i> * ((Im y)))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - (<i> * (((Im x)),(<i> * ((Im y))))))) is complex Element of COMPLEX
addcomplex $$ (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + ((<i> * (((Im x)),((Re y)))) - (<i> * (((Im x)),(<i> * ((Im y))))))) is complex Element of COMPLEX
(((Im x)),((Re y))) - (((Im x)),(<i> * ((Im y)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
K385((((Im x)),(<i> * ((Im y))))) is V1() Function-like complex-yielding set
(- 1) * (((Im x)),(<i> * ((Im y)))) is V1() Function-like set
K356((((Im x)),((Re y))),K385((((Im x)),(<i> * ((Im y)))))) is V1() Function-like set
<i> * ((((Im x)),((Re y))) - (((Im x)),(<i> * ((Im y))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * ((((Im x)),((Re y))) - (((Im x)),(<i> * ((Im y)))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * ((((Im x)),((Re y))) - (((Im x)),(<i> * ((Im y))))))) is complex Element of COMPLEX
addcomplex $$ (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * ((((Im x)),((Re y))) - (((Im x)),(<i> * ((Im y))))))) is complex Element of COMPLEX
(((Im x)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Im x)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
<i> * (((Im x)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * (((Im x)),(y *'))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * (((Im x)),(y *')))) is complex Element of COMPLEX
addcomplex $$ (((((Re x)),((Re y))) - (((Re x)),(<i> * ((Im y))))) + (<i> * (((Im x)),(y *')))) is complex Element of COMPLEX
(((Re x)),(((Re y)) - (<i> * ((Im y))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Re x)),(((Re y)) - (<i> * ((Im y))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(((Re x)),(((Re y)) - (<i> * ((Im y))))) + (<i> * (((Im x)),(y *'))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((((Re x)),(((Re y)) - (<i> * ((Im y))))) + (<i> * (((Im x)),(y *')))) is complex Element of COMPLEX
addcomplex $$ ((((Re x)),(((Re y)) - (<i> * ((Im y))))) + (<i> * (((Im x)),(y *')))) is complex Element of COMPLEX
(((Re x)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Re x)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((<i> * ((Im x))),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((<i> * ((Im x))),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(((Re x)),(y *')) + ((<i> * ((Im x))),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((((Re x)),(y *')) + ((<i> * ((Im x))),(y *'))) is complex Element of COMPLEX
addcomplex $$ ((((Re x)),(y *')) + ((<i> * ((Im x))),(y *'))) is complex Element of COMPLEX
y is ordinal natural complex ext-real non negative set
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
M + i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
Line ((M + i),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (M + i)) FinSequence-like complex-yielding Element of (width (M + i)) -tuples_on COMPLEX
width (M + i) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width (M + i)) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Line (M,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width M) FinSequence-like complex-yielding Element of (width M) -tuples_on COMPLEX
(width M) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Line (i,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width i) FinSequence-like complex-yielding Element of (width i) -tuples_on COMPLEX
(width i) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(Line (M,y)) + (Line (i,y)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (Line (i,y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (Line (M,y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((Line (M,y)) + (Line (i,y))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (Line ((M + i),y)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is ordinal natural complex ext-real non negative set
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[y,j] is set
[:(Seg (len M)),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Seg (len ((Line (M,y)) + (Line (i,y)))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom ((Line (M,y)) + (Line (i,y))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (M + i)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(Line ((M + i),y)) . j is complex Element of COMPLEX
(M + i) * (y,j) is complex Element of COMPLEX
M * (y,j) is complex Element of COMPLEX
i * (y,j) is complex Element of COMPLEX
(M * (y,j)) + (i * (y,j)) is complex Element of COMPLEX
(Line (i,y)) . j is complex Element of COMPLEX
(M * (y,j)) + ((Line (i,y)) . j) is complex Element of COMPLEX
(Line (M,y)) . j is complex Element of COMPLEX
((Line (M,y)) . j) + ((Line (i,y)) . j) is complex Element of COMPLEX
((Line (M,y)) + (Line (i,y))) . j is complex Element of COMPLEX
x is ordinal natural complex ext-real non negative set
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Line (y,x) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width y) FinSequence-like complex-yielding Element of (width y) -tuples_on COMPLEX
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
Line ((y),x) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (y)) FinSequence-like complex-yielding Element of (width (y)) -tuples_on COMPLEX
width (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width (y)) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(Line ((y),x)) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (Line (y,x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((Line ((y),x)) *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (Line ((y),x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is ordinal natural complex ext-real non negative set
(Line (y,x)) . M is complex Element of COMPLEX
((Line ((y),x)) *') . M is complex Element of COMPLEX
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[x,M] is set
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg (width y)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
y * (x,M) is complex Element of COMPLEX
(y * (x,M)) *' is complex Element of COMPLEX
((y * (x,M)) *') *' is complex Element of COMPLEX
(y) * (x,M) is complex Element of COMPLEX
((y) * (x,M)) *' is complex Element of COMPLEX
(Line ((y),x)) . M is complex Element of COMPLEX
((Line ((y),x)) . M) *' is complex Element of COMPLEX
x is ordinal natural complex ext-real non negative set
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
Line ((M),x) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (M)) FinSequence-like complex-yielding Element of (width (M)) -tuples_on COMPLEX
width (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width (M)) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(Line ((M),x)) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y,((Line ((M),x)) *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,((Line ((M),x)) *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((Line ((M),x)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((Line ((M),x)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((Line ((M),x)),(y *')) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (Line ((M),x)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y,x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y,x) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(y) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((y),(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((y,x) *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y,x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is ordinal natural complex ext-real non negative set
Seg (len y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Line ((y),M) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (y)) FinSequence-like complex-yielding Element of (width (y)) -tuples_on COMPLEX
(width (y)) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Line ((y),M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((Line ((y),M)),(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((Line ((y),M)),(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((Line ((y),M)),(x *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (y)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((y,x) *') . M is complex Element of COMPLEX
(y,x) . M is complex Element of COMPLEX
((y,x) . M) *' is complex Element of COMPLEX
Line (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width y) FinSequence-like complex-yielding Element of (width y) -tuples_on COMPLEX
(width y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(x,(Line (y,M))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(Line (y,M))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x,(Line (y,M))) is complex Element of COMPLEX
addcomplex $$ (x,(Line (y,M))) is complex Element of COMPLEX
(Sum (x,(Line (y,M)))) *' is complex Element of COMPLEX
(Line ((y),M)) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,((Line ((y),M)) *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,((Line ((y),M)) *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x,((Line ((y),M)) *')) is complex Element of COMPLEX
addcomplex $$ (x,((Line ((y),M)) *')) is complex Element of COMPLEX
(Sum (x,((Line ((y),M)) *'))) *' is complex Element of COMPLEX
((Line ((y),M)),(x *')) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((Line ((y),M)),(x *')) *') is complex Element of COMPLEX
addcomplex $$ (((Line ((y),M)),(x *')) *') is complex Element of COMPLEX
(Sum (((Line ((y),M)),(x *')) *')) *' is complex Element of COMPLEX
Sum ((Line ((y),M)),(x *')) is complex Element of COMPLEX
addcomplex $$ ((Line ((y),M)),(x *')) is complex Element of COMPLEX
(Sum ((Line ((y),M)),(x *'))) *' is complex Element of COMPLEX
((Sum ((Line ((y),M)),(x *'))) *') *' is complex Element of COMPLEX
((y),(x *')) . M is complex Element of COMPLEX
len ((y),(x *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,(y,M)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(y,M)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((x,y),M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((x,y),M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(len M) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
i9 is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
j is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len y) FinSequence-like complex-yielding Element of (len y) -tuples_on COMPLEX
multcomplex .: (i9,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
i is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len M) FinSequence-like complex-yielding Element of (len M) -tuples_on COMPLEX
multcomplex .: ((multcomplex .: (i9,j)),i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
- x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
- 1 is non zero complex set
(- 1) * x is V1() Function-like set
Sum (- x) is complex Element of COMPLEX
addcomplex $$ (- x) is complex Element of COMPLEX
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
- (Sum x) is complex Element of COMPLEX
compcomplex * x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
addcomplex $$ (compcomplex * x) is complex Element of COMPLEX
compcomplex . (addcomplex $$ x) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x ^ y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x ^ y) is complex Element of COMPLEX
addcomplex $$ (x ^ y) is complex Element of COMPLEX
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
Sum y is complex Element of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
(Sum x) + (Sum y) is complex Element of COMPLEX
addcomplex . ((addcomplex $$ x),(addcomplex $$ y)) is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
M is ordinal natural complex ext-real non negative set
y . M is complex Element of COMPLEX
Line (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width x) FinSequence-like complex-yielding Element of (width x) -tuples_on COMPLEX
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Sum (Line (x,M)) is complex Element of COMPLEX
addcomplex $$ (Line (x,M)) is complex Element of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is ordinal natural complex ext-real non negative set
y . i is complex Element of COMPLEX
M . i is complex Element of COMPLEX
Line (x,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width x) FinSequence-like complex-yielding Element of (width x) -tuples_on COMPLEX
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Sum (Line (x,i)) is complex Element of COMPLEX
addcomplex $$ (Line (x,i)) is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
M is ordinal natural complex ext-real non negative set
y . M is complex Element of COMPLEX
Col (x,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Sum (Col (x,M)) is complex Element of COMPLEX
addcomplex $$ (Col (x,M)) is complex Element of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
i is ordinal natural complex ext-real non negative set
y . i is complex Element of COMPLEX
M . i is complex Element of COMPLEX
Col (x,i) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Sum (Col (x,i)) is complex Element of COMPLEX
addcomplex $$ (Col (x,i)) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
x . 1 is complex Element of COMPLEX
<*(x . 1)*> is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum x is complex Element of COMPLEX
addcomplex $$ x is complex Element of COMPLEX
Sum y is complex Element of COMPLEX
addcomplex $$ y is complex Element of COMPLEX
x /. (len x) is complex Element of COMPLEX
(Sum y) + (x /. (len x)) is complex Element of COMPLEX
M is ordinal natural complex ext-real non negative set
M + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x | M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (M + 1) is V162() V163() V164() V165() V166() V167() Element of bool NAT
<*(x /. (len x))*> is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y ^ <*(x /. (len x))*> is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len <*(x /. (len x))*> is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg M is V162() V163() V164() V165() V166() V167() Element of bool NAT
x | (Seg M) is V1() V4( NAT ) V5( COMPLEX ) Function-like complex-yielding Element of bool [:NAT,COMPLEX:]
j9 is set
{ b₁ where b₁ is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT : ( 1 <= b₁ & b₁ <= M + 1 ) } is set
n3 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len y) + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len y) + (len <*(x /. (len x))*>) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y ^ <*(x /. (len x))*>) . n3 is complex Element of COMPLEX
n3 - (len y) is V52() V107() complex ext-real V161() Element of INT
<*(x /. (len x))*> . (n3 - (len y)) is complex Element of COMPLEX
(M + 1) - M is complex Element of COMPLEX
<*(x /. (len x))*> . ((M + 1) - M) is complex Element of COMPLEX
x /. (M + 1) is complex Element of COMPLEX
x . n3 is complex Element of COMPLEX
{ b₁ where b₁ is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT : ( 1 <= b₁ & b₁ <= M ) } is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
(y ^ <*(x /. (len x))*>) . n3 is complex Element of COMPLEX
y . n3 is complex Element of COMPLEX
x . n3 is complex Element of COMPLEX
(y ^ <*(x /. (len x))*>) . n3 is complex Element of COMPLEX
x . n3 is complex Element of COMPLEX
(y ^ <*(x /. (len x))*>) . n3 is complex Element of COMPLEX
x . n3 is complex Element of COMPLEX
x . j9 is complex Element of COMPLEX
(y ^ <*(x /. (len x))*>) . j9 is complex Element of COMPLEX
len (y ^ <*(x /. (len x))*>) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len y) + (len <*(x /. (len x))*>) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len y) + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (y ^ <*(x /. (len x))*>)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (y ^ <*(x /. (len x))*>) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Sum <*(x /. (len x))*> is complex Element of COMPLEX
addcomplex $$ <*(x /. (len x))*> is complex Element of COMPLEX
(Sum y) + (Sum <*(x /. (len x))*>) is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x) is complex Element of COMPLEX
addcomplex $$ (x) is complex Element of COMPLEX
(x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x) is complex Element of COMPLEX
addcomplex $$ (x) is complex Element of COMPLEX
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(0 + 1) - 1 is V52() V107() complex ext-real V161() Element of INT
(len x) - 1 is V52() V107() complex ext-real V161() Element of INT
(len x) -' 1 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is ordinal natural complex ext-real non negative set
y + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y + 1) + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (i) is complex Element of COMPLEX
addcomplex $$ (i) is complex Element of COMPLEX
(i) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (i) is complex Element of COMPLEX
addcomplex $$ (i) is complex Element of COMPLEX
rng i is functional Element of bool (COMPLEX *)
bool (COMPLEX *) is set
j is ordinal natural complex ext-real non negative set
M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i | M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like FinSequence of COMPLEX *
rng (i | M) is functional Element of bool (COMPLEX *)
i9 is set
i9 is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
n3 is ordinal natural complex ext-real non negative set
Line (i,((y + 1) + 1)) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width i) FinSequence-like complex-yielding Element of (width i) -tuples_on COMPLEX
width i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width i) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Line (i,((y + 1) + 1))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len i9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
1 + y is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len i9) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom i9 is V162() V163() V164() V165() V166() V167() Element of bool NAT
i9 . 1 is V1() Function-like set
rng i9 is functional Element of bool (COMPLEX *)
width i9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is V1() Function-like FinSequence-like set
len j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
i . 1 is V1() Function-like set
j is V1() Function-like FinSequence-like set
len j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (i) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(i) | M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((i) | M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is ordinal natural complex ext-real non negative set
((i) | M) . j is complex Element of COMPLEX
(i9) . j is complex Element of COMPLEX
Line (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width i) FinSequence-like complex-yielding Element of (width i) -tuples_on COMPLEX
len (Line (i,j)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Line (i9,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width i9) FinSequence-like complex-yielding Element of (width i9) -tuples_on COMPLEX
(width i9) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
i9 . j is V1() Function-like set
i . j is V1() Function-like set
g is ordinal natural complex ext-real non negative set
(Line (i,j)) . g is complex Element of COMPLEX
(Line (i9,j)) . g is complex Element of COMPLEX
Seg (len (Line (i,j))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width i9) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[j,g] is set
Indices i is set
[:(dom i),(Seg (width i)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i * (j,g) is complex Element of COMPLEX
f is V1() Function-like FinSequence-like set
len f is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices i9 is set
[:(dom i9),(Seg (width i9)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i9 * (j,g) is complex Element of COMPLEX
f is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
f . g is complex Element of COMPLEX
len (Line (i9,j)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
g is V1() Function-like FinSequence-like set
len g is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((i) | M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom ((i) | M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg M is V162() V163() V164() V165() V166() V167() Element of bool NAT
(i) | (Seg M) is V1() V4( NAT ) V5( COMPLEX ) Function-like complex-yielding Element of bool [:NAT,COMPLEX:]
dom ((i) | (Seg M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((i) | (Seg M)) . j is complex Element of COMPLEX
(i) . j is complex Element of COMPLEX
Sum (Line (i9,j)) is complex Element of COMPLEX
addcomplex $$ (Line (i9,j)) is complex Element of COMPLEX
(i9) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (i9) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(i9) + (Line (i,((y + 1) + 1))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((i9) + (Line (i,((y + 1) + 1)))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (i) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is V1() Function-like FinSequence-like set
len j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (i)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
j is ordinal natural complex ext-real non negative set
(i9) . j is complex Element of COMPLEX
i * (((y + 1) + 1),j) is complex Element of COMPLEX
((i9) . j) + (i * (((y + 1) + 1),j)) is complex Element of COMPLEX
(i) . j is complex Element of COMPLEX
Col (i9,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len i9) FinSequence-like complex-yielding Element of (len i9) -tuples_on COMPLEX
(len i9) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Col (i,j) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len i) FinSequence-like complex-yielding Element of (len i) -tuples_on COMPLEX
(len i) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Col (i,j)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(Col (i,j)) | M is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((Col (i,j)) | M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
n is ordinal natural complex ext-real non negative set
((Col (i,j)) | M) . n is complex Element of COMPLEX
(Col (i9,j)) . n is complex Element of COMPLEX
i9 . n is V1() Function-like set
i . n is V1() Function-like set
[n,j] is set
Indices i is set
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i),(Seg (width i)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i * (n,j) is complex Element of COMPLEX
c₁₄ is V1() Function-like FinSequence-like set
len c₁₄ is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg M is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len ((Col (i,j)) | M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom ((Col (i,j)) | M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(Col (i,j)) | (Seg M) is V1() V4( NAT ) V5( COMPLEX ) Function-like complex-yielding Element of bool [:NAT,COMPLEX:]
dom ((Col (i,j)) | (Seg M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Indices i9 is set
Seg (width i9) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i9),(Seg (width i9)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
((Col (i,j)) | (Seg M)) . n is complex Element of COMPLEX
(Col (i,j)) . n is complex Element of COMPLEX
i9 * (n,j) is complex Element of COMPLEX
c₁₄ is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
c₁₄ . j is complex Element of COMPLEX
len (Col (i9,j)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (Col (i,j))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (Col (i,j)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Sum (Col (i9,j)) is complex Element of COMPLEX
addcomplex $$ (Col (i9,j)) is complex Element of COMPLEX
(Sum (Col (i9,j))) + (i * (((y + 1) + 1),j)) is complex Element of COMPLEX
(Col (i,j)) . ((y + 1) + 1) is complex Element of COMPLEX
(Sum (Col (i9,j))) + ((Col (i,j)) . ((y + 1) + 1)) is complex Element of COMPLEX
(Col (i,j)) /. ((y + 1) + 1) is complex Element of COMPLEX
(Sum (Col (i9,j))) + ((Col (i,j)) /. ((y + 1) + 1)) is complex Element of COMPLEX
Sum (Col (i,j)) is complex Element of COMPLEX
addcomplex $$ (Col (i,j)) is complex Element of COMPLEX
j is ordinal natural complex ext-real non negative set
((i9) + (Line (i,((y + 1) + 1)))) . j is complex Element of COMPLEX
(i) . j is complex Element of COMPLEX
Seg (len (i)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width i9) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len ((i9) + (Line (i,((y + 1) + 1))))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom ((i9) + (Line (i,((y + 1) + 1)))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(i9) . j is complex Element of COMPLEX
(Line (i,((y + 1) + 1))) . j is complex Element of COMPLEX
((i9) . j) + ((Line (i,((y + 1) + 1))) . j) is complex Element of COMPLEX
i * (((y + 1) + 1),j) is complex Element of COMPLEX
((i9) . j) + (i * (((y + 1) + 1),j)) is complex Element of COMPLEX
Sum (i9) is complex Element of COMPLEX
addcomplex $$ (i9) is complex Element of COMPLEX
(i) /. ((y + 1) + 1) is complex Element of COMPLEX
(Sum (i9)) + ((i) /. ((y + 1) + 1)) is complex Element of COMPLEX
(i) . ((y + 1) + 1) is complex Element of COMPLEX
(Sum (i9)) + ((i) . ((y + 1) + 1)) is complex Element of COMPLEX
Sum (i9) is complex Element of COMPLEX
addcomplex $$ (i9) is complex Element of COMPLEX
(Sum (i9)) + ((i) . ((y + 1) + 1)) is complex Element of COMPLEX
Sum (Line (i,((y + 1) + 1))) is complex Element of COMPLEX
addcomplex $$ (Line (i,((y + 1) + 1))) is complex Element of COMPLEX
(Sum (i9)) + (Sum (Line (i,((y + 1) + 1)))) is complex Element of COMPLEX
Sum ((i9) + (Line (i,((y + 1) + 1)))) is complex Element of COMPLEX
addcomplex $$ ((i9) + (Line (i,((y + 1) + 1)))) is complex Element of COMPLEX
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (M) is complex Element of COMPLEX
addcomplex $$ (M) is complex Element of COMPLEX
(M) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (M) is complex Element of COMPLEX
addcomplex $$ (M) is complex Element of COMPLEX
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (y) is complex Element of COMPLEX
addcomplex $$ (y) is complex Element of COMPLEX
(y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (y) is complex Element of COMPLEX
addcomplex $$ (y) is complex Element of COMPLEX
Line (y,1) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width y) FinSequence-like complex-yielding Element of (width y) -tuples_on COMPLEX
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Line (y,1)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg 1 is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
M is ordinal natural complex ext-real non negative set
(y) . M is complex Element of COMPLEX
(Line (y,1)) . M is complex Element of COMPLEX
Col (y,M) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len y) FinSequence-like complex-yielding Element of (len y) -tuples_on COMPLEX
(len y) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Col (y,M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Sum (Col (y,M)) is complex Element of COMPLEX
addcomplex $$ (Col (y,M)) is complex Element of COMPLEX
(Col (y,M)) . 1 is complex Element of COMPLEX
y * (1,M) is complex Element of COMPLEX
len (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Sum (Line (y,1)) is complex Element of COMPLEX
addcomplex $$ (Line (y,1)) is complex Element of COMPLEX
(y) . 1 is complex Element of COMPLEX
y is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (y) is complex Element of COMPLEX
addcomplex $$ (y) is complex Element of COMPLEX
(y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (y) is complex Element of COMPLEX
addcomplex $$ (y) is complex Element of COMPLEX
((len x) -' 1) + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x) is complex Element of COMPLEX
addcomplex $$ (x) is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x @)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x @)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is ordinal natural complex ext-real non negative set
Seg (len ((x @))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len (x @)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(x) . y is complex Element of COMPLEX
Col (x,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( len x) FinSequence-like complex-yielding Element of (len x) -tuples_on COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(len x) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Sum (Col (x,y)) is complex Element of COMPLEX
addcomplex $$ (Col (x,y)) is complex Element of COMPLEX
Line ((x @),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (x @)) FinSequence-like complex-yielding Element of (width (x @)) -tuples_on COMPLEX
width (x @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width (x @)) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
Sum (Line ((x @),y)) is complex Element of COMPLEX
addcomplex $$ (Line ((x @),y)) is complex Element of COMPLEX
((x @)) . y is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x) is complex Element of COMPLEX
(x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x) is complex Element of COMPLEX
addcomplex $$ (x) is complex Element of COMPLEX
x @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x @)) is complex Element of COMPLEX
((x @)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((x @)) is complex Element of COMPLEX
addcomplex $$ ((x @)) is complex Element of COMPLEX
(x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x) is complex Element of COMPLEX
addcomplex $$ (x) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular Matrix of len M, width M, COMPLEX
Indices i is set
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
width i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i),(Seg (width i)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is ordinal natural complex ext-real non negative set
i9 is ordinal natural complex ext-real non negative set
[j,i9] is set
i * (j,i9) is complex Element of COMPLEX
x . j is complex Element of COMPLEX
M * (j,i9) is complex Element of COMPLEX
(x . j) * (M * (j,i9)) is complex Element of COMPLEX
y . i9 is complex Element of COMPLEX
(y . i9) *' is complex Element of COMPLEX
((x . j) * (M * (j,i9))) * ((y . i9) *') is complex Element of COMPLEX
i is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width i is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i9 is ordinal natural complex ext-real non negative set
j9 is ordinal natural complex ext-real non negative set
[i9,j9] is set
Indices i is set
dom i is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width i) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i),(Seg (width i)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i * (i9,j9) is complex Element of COMPLEX
x . i9 is complex Element of COMPLEX
M * (i9,j9) is complex Element of COMPLEX
(x . i9) * (M * (i9,j9)) is complex Element of COMPLEX
y . j9 is complex Element of COMPLEX
(y . j9) *' is complex Element of COMPLEX
((x . i9) * (M * (i9,j9))) * ((y . j9) *') is complex Element of COMPLEX
j * (i9,j9) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x,y,M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x,y,M) @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
M @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(y,x,(M)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((y,x,(M))) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (M @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x,y,M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x,y,M) @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x,y,M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x,y,M) @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (y,x,(M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((y,x,(M))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y,x,(M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices ((x,y,M) @) is set
dom ((x,y,M) @) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width ((x,y,M) @)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ((x,y,M) @)),(Seg (width ((x,y,M) @))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i is ordinal natural complex ext-real non negative set
j is ordinal natural complex ext-real non negative set
[i,j] is set
((y,x,(M))) * (i,j) is complex Element of COMPLEX
((x,y,M) @) * (i,j) is complex Element of COMPLEX
[j,i] is set
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (x,y,M) is set
dom (x,y,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x,y,M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x,y,M)),(Seg (width (x,y,M))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (M) is set
dom (M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (M)),(Seg (width (M))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (y,x,(M)) is set
dom (y,x,(M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (y,x,(M))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (y,x,(M))),(Seg (width (y,x,(M)))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
(y,x,(M)) * (i,j) is complex Element of COMPLEX
((y,x,(M)) * (i,j)) *' is complex Element of COMPLEX
y . i is complex Element of COMPLEX
(M) * (i,j) is complex Element of COMPLEX
(y . i) * ((M) * (i,j)) is complex Element of COMPLEX
x . j is complex Element of COMPLEX
(x . j) *' is complex Element of COMPLEX
((y . i) * ((M) * (i,j))) * ((x . j) *') is complex Element of COMPLEX
(((y . i) * ((M) * (i,j))) * ((x . j) *')) *' is complex Element of COMPLEX
i9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M) * (i9,j9) is complex Element of COMPLEX
(y . i) * ((M) * (i9,j9)) is complex Element of COMPLEX
(x *') . j is complex Element of COMPLEX
((y . i) * ((M) * (i9,j9))) * ((x *') . j) is complex Element of COMPLEX
(((y . i) * ((M) * (i9,j9))) * ((x *') . j)) *' is complex Element of COMPLEX
((y . i) * ((M) * (i,j))) *' is complex Element of COMPLEX
((x *') . j) *' is complex Element of COMPLEX
(((y . i) * ((M) * (i,j))) *') * (((x *') . j) *') is complex Element of COMPLEX
((y . i) * ((M) * (i9,j9))) *' is complex Element of COMPLEX
(x *') *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((x *') *') . j is complex Element of COMPLEX
(((y . i) * ((M) * (i9,j9))) *') * (((x *') *') . j) is complex Element of COMPLEX
(y . i) *' is complex Element of COMPLEX
((M) * (i,j)) *' is complex Element of COMPLEX
((y . i) *') * (((M) * (i,j)) *') is complex Element of COMPLEX
(((y . i) *') * (((M) * (i,j)) *')) * (((x *') *') . j) is complex Element of COMPLEX
((M)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M)) * (i,j) is complex Element of COMPLEX
((y . i) *') * (((M)) * (i,j)) is complex Element of COMPLEX
(((y . i) *') * (((M)) * (i,j))) * (((x *') *') . j) is complex Element of COMPLEX
(((y . i) *') * (((M)) * (i,j))) * (x . j) is complex Element of COMPLEX
(M @) * (i,j) is complex Element of COMPLEX
((y . i) *') * ((M @) * (i,j)) is complex Element of COMPLEX
(((y . i) *') * ((M @) * (i,j))) * (x . j) is complex Element of COMPLEX
M * (j,i) is complex Element of COMPLEX
((y . i) *') * (M * (j,i)) is complex Element of COMPLEX
(((y . i) *') * (M * (j,i))) * (x . j) is complex Element of COMPLEX
(x . j) * (M * (j,i)) is complex Element of COMPLEX
((x . j) * (M * (j,i))) * ((y . i) *') is complex Element of COMPLEX
(x,y,M) * (j,i) is complex Element of COMPLEX
width ((y,x,(M))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x,y,M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x,y,M)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x *'),(y *'),(M)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len (y *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x *'),(y *'),(M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x,y,M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x,y,M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x,y,M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x,y,M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices ((x,y,M)) is set
dom ((x,y,M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width ((x,y,M))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ((x,y,M))),(Seg (width ((x,y,M)))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
i is ordinal natural complex ext-real non negative set
j is ordinal natural complex ext-real non negative set
[i,j] is set
((x,y,M)) * (i,j) is complex Element of COMPLEX
((x *'),(y *'),(M)) * (i,j) is complex Element of COMPLEX
Indices (M) is set
dom (M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (M)),(Seg (width (M))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices M is set
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg (width M)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (x,y,M) is set
dom (x,y,M) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x,y,M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x,y,M)),(Seg (width (x,y,M))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
(x,y,M) * (i,j) is complex Element of COMPLEX
((x,y,M) * (i,j)) *' is complex Element of COMPLEX
x . i is complex Element of COMPLEX
M * (i,j) is complex Element of COMPLEX
(x . i) * (M * (i,j)) is complex Element of COMPLEX
y . j is complex Element of COMPLEX
(y . j) *' is complex Element of COMPLEX
((x . i) * (M * (i,j))) * ((y . j) *') is complex Element of COMPLEX
(((x . i) * (M * (i,j))) * ((y . j) *')) *' is complex Element of COMPLEX
i9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j9 is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M * (i9,j9) is complex Element of COMPLEX
(x . i) * (M * (i9,j9)) is complex Element of COMPLEX
(y *') . j is complex Element of COMPLEX
((x . i) * (M * (i9,j9))) * ((y *') . j) is complex Element of COMPLEX
(((x . i) * (M * (i9,j9))) * ((y *') . j)) *' is complex Element of COMPLEX
((x . i) * (M * (i,j))) *' is complex Element of COMPLEX
((y *') . j) *' is complex Element of COMPLEX
(((x . i) * (M * (i,j))) *') * (((y *') . j) *') is complex Element of COMPLEX
((x . i) * (M * (i9,j9))) *' is complex Element of COMPLEX
(y *') *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((y *') *') . j is complex Element of COMPLEX
(((x . i) * (M * (i9,j9))) *') * (((y *') *') . j) is complex Element of COMPLEX
(x . i) *' is complex Element of COMPLEX
(M * (i,j)) *' is complex Element of COMPLEX
((x . i) *') * ((M * (i,j)) *') is complex Element of COMPLEX
(((x . i) *') * ((M * (i,j)) *')) * (((y *') *') . j) is complex Element of COMPLEX
(M) * (i,j) is complex Element of COMPLEX
((x . i) *') * ((M) * (i,j)) is complex Element of COMPLEX
(((x . i) *') * ((M) * (i,j))) * (((y *') *') . j) is complex Element of COMPLEX
(M) * (i9,j9) is complex Element of COMPLEX
((x . i) *') * ((M) * (i9,j9)) is complex Element of COMPLEX
(((x . i) *') * ((M) * (i9,j9))) * (((y *') . j) *') is complex Element of COMPLEX
(x *') . i is complex Element of COMPLEX
((x *') . i) * ((M) * (i9,j9)) is complex Element of COMPLEX
(((x *') . i) * ((M) * (i9,j9))) * (((y *') . j) *') is complex Element of COMPLEX
width ((x *'),(y *'),(M)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
|(x,y)| is complex Element of COMPLEX
|(y,x)| is complex Element of COMPLEX
|(y,x)| *' is complex Element of COMPLEX
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y,(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (y,(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (y,(x *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Sum (y,(x *')) is complex Element of COMPLEX
addcomplex $$ (y,(x *')) is complex Element of COMPLEX
(Sum (y,(x *'))) *' is complex Element of COMPLEX
(y,(x *')) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((y,(x *')) *') is complex Element of COMPLEX
addcomplex $$ ((y,(x *')) *') is complex Element of COMPLEX
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (x,(y *')) is complex Element of COMPLEX
addcomplex $$ (x,(y *')) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
|(x,y)| is complex Element of COMPLEX
|(x,y)| *' is complex Element of COMPLEX
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|((x *'),(y *'))| is complex Element of COMPLEX
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (y *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x,(y *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(y *') *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
((x *'),((y *') *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((x *'),((y *') *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((x *'),((y *') *')) is complex Element of COMPLEX
addcomplex $$ ((x *'),((y *') *')) is complex Element of COMPLEX
(x,(y *')) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((x,(y *')) *') is complex Element of COMPLEX
addcomplex $$ ((x,(y *')) *') is complex Element of COMPLEX
Sum (x,(y *')) is complex Element of COMPLEX
addcomplex $$ (x,(y *')) is complex Element of COMPLEX
(Sum (x,(y *'))) *' is complex Element of COMPLEX
x is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x) @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width (x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x) @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((x @)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (x @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((x @)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (x @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Indices ((x @)) is set
dom ((x @)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width ((x @))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ((x @))),(Seg (width ((x @)))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
y is ordinal natural complex ext-real non negative set
M is ordinal natural complex ext-real non negative set
[y,M] is set
((x @)) * (y,M) is complex Element of COMPLEX
((x) @) * (y,M) is complex Element of COMPLEX
Indices (x @) is set
dom (x @) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x @)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x @)),(Seg (width (x @))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
[M,y] is set
Indices x is set
dom x is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg (width x)):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
Indices (x) is set
dom (x) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (x)),(Seg (width (x))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
(x @) * (y,M) is complex Element of COMPLEX
((x @) * (y,M)) *' is complex Element of COMPLEX
x * (M,y) is complex Element of COMPLEX
(x * (M,y)) *' is complex Element of COMPLEX
(x) * (M,y) is complex Element of COMPLEX
len ((x) @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
M @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|(x,((M),y))| is complex Element of COMPLEX
(x,y,(M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x,y,(M @))) is complex Element of COMPLEX
((x,y,(M @))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((x,y,(M @))) is complex Element of COMPLEX
addcomplex $$ ((x,y,(M @))) is complex Element of COMPLEX
width (M @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width ((M @)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
dom ((x,y,(M @))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len ((x,y,(M @))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((x,y,(M @)))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len (x,y,(M @)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (x,y,(M @))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
len (M @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len ((M),y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((M),y) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (((M),y) *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(x,(((M),y) *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (x,(((M),y) *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x,(((M),y) *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
i is ordinal natural complex ext-real non negative set
((x,y,(M @))) . i is complex Element of COMPLEX
(x,(((M),y) *')) . i is complex Element of COMPLEX
width (x,y,(M @)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Line ((x,y,(M @)),i) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (x,y,(M @))) FinSequence-like complex-yielding Element of (width (x,y,(M @))) -tuples_on COMPLEX
(width (x,y,(M @))) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Line ((x,y,(M @)),i)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Line ((M),i) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (M)) FinSequence-like complex-yielding Element of (width (M)) -tuples_on COMPLEX
width (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(width (M)) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Line ((M),i)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((Line ((M),i)),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((Line ((M),i)),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((Line ((M),i)),y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (M)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((Line ((M),i)),y) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
x . i is complex Element of COMPLEX
(x . i) * (((Line ((M),i)),y) *') is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Line ((M @),i) is V1() V4( NAT ) V5( COMPLEX ) Function-like V40( width (M @)) FinSequence-like complex-yielding Element of (width (M @)) -tuples_on COMPLEX
(width (M @)) -tuples_on COMPLEX is functional non zero FinSequence-membered FinSequenceSet of COMPLEX
len (Line ((M @),i)) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (y *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
j is ordinal natural complex ext-real non negative set
((x . i) * (((Line ((M),i)),y) *')) . j is complex Element of COMPLEX
(Line ((x,y,(M @)),i)) . j is complex Element of COMPLEX
Seg (width (M @)) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len y) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len (y *')) is V162() V163() V164() V165() V166() V167() Element of bool NAT
((Line ((M @),i)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: ((Line ((M @),i)),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len ((Line ((M @),i)),(y *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len ((Line ((M @),i)),(y *'))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom ((Line ((M @),i)),(y *')) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (len (Line ((x,y,(M @)),i))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg (width (x,y,(M @))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[i,j] is set
Indices (M @) is set
dom (M @) is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom (M @)),(Seg (width (M @))):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
(((Line ((M),i)),y) *') . j is complex Element of COMPLEX
(x . i) * ((((Line ((M),i)),y) *') . j) is complex Element of COMPLEX
(Line ((M),i)) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(((Line ((M),i)) *'),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
multcomplex .: (((Line ((M),i)) *'),(y *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
(((Line ((M),i)) *'),(y *')) . j is complex Element of COMPLEX
(x . i) * ((((Line ((M),i)) *'),(y *')) . j) is complex Element of COMPLEX
((Line ((M @),i)),(y *')) . j is complex Element of COMPLEX
(x . i) * (((Line ((M @),i)),(y *')) . j) is complex Element of COMPLEX
(Line ((M @),i)) . j is complex Element of COMPLEX
(y *') . j is complex Element of COMPLEX
((Line ((M @),i)) . j) * ((y *') . j) is complex Element of COMPLEX
(x . i) * (((Line ((M @),i)) . j) * ((y *') . j)) is complex Element of COMPLEX
y . j is complex Element of COMPLEX
(y . j) *' is complex Element of COMPLEX
((Line ((M @),i)) . j) * ((y . j) *') is complex Element of COMPLEX
(x . i) * (((Line ((M @),i)) . j) * ((y . j) *')) is complex Element of COMPLEX
(x . i) * ((Line ((M @),i)) . j) is complex Element of COMPLEX
((x . i) * ((Line ((M @),i)) . j)) * ((y . j) *') is complex Element of COMPLEX
(M @) * (i,j) is complex Element of COMPLEX
(x . i) * ((M @) * (i,j)) is complex Element of COMPLEX
((x . i) * ((M @) * (i,j))) * ((y . j) *') is complex Element of COMPLEX
(x,y,(M @)) * (i,j) is complex Element of COMPLEX
len ((x . i) * (((Line ((M),i)),y) *')) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (((Line ((M),i)),y) *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg (len (x,(((M),y) *'))) is V162() V163() V164() V165() V166() V167() Element of bool NAT
dom (x,(((M),y) *')) is V162() V163() V164() V165() V166() V167() Element of bool NAT
(((M),y) *') . i is complex Element of COMPLEX
(x . i) * ((((M),y) *') . i) is complex Element of COMPLEX
((M),y) . i is complex Element of COMPLEX
(((M),y) . i) *' is complex Element of COMPLEX
(x . i) * ((((M),y) . i) *') is complex Element of COMPLEX
Sum ((Line ((M),i)),y) is complex Element of COMPLEX
addcomplex $$ ((Line ((M),i)),y) is complex Element of COMPLEX
(Sum ((Line ((M),i)),y)) *' is complex Element of COMPLEX
(x . i) * ((Sum ((Line ((M),i)),y)) *') is complex Element of COMPLEX
Sum (((Line ((M),i)),y) *') is complex Element of COMPLEX
addcomplex $$ (((Line ((M),i)),y) *') is complex Element of COMPLEX
(x . i) * (Sum (((Line ((M),i)),y) *')) is complex Element of COMPLEX
Sum ((x . i) * (((Line ((M),i)),y) *')) is complex Element of COMPLEX
addcomplex $$ ((x . i) * (((Line ((M),i)),y) *')) is complex Element of COMPLEX
Sum (Line ((x,y,(M @)),i)) is complex Element of COMPLEX
addcomplex $$ (Line ((x,y,(M @)),i)) is complex Element of COMPLEX
Sum (x,(((M),y) *')) is complex Element of COMPLEX
addcomplex $$ (x,(((M),y) *')) is complex Element of COMPLEX
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M,x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|((M,x),y)| is complex Element of COMPLEX
M @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(x,y,(M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x,y,(M @))) is complex Element of COMPLEX
((x,y,(M @))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((x,y,(M @))) is complex Element of COMPLEX
addcomplex $$ ((x,y,(M @))) is complex Element of COMPLEX
((M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(M @) @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(((M @) @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width (M @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
x *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (x *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len (y *') is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
((y *'),(x *'),M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len ((y *'),(x *'),M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
0 + 1 is non zero ordinal natural V52() V107() complex ext-real positive non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M,x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
|(y,(M,x))| is complex Element of COMPLEX
|(y,(M,x))| *' is complex Element of COMPLEX
(M,x) *' is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|((y *'),((M,x) *'))| is complex Element of COMPLEX
((M),(x *')) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|((y *'),((M),(x *')))| is complex Element of COMPLEX
((y *'),(x *'),((M @) @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(((y *'),(x *'),((M @) @))) is complex Element of COMPLEX
(((y *'),(x *'),((M @) @))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((y *'),(x *'),((M @) @))) is complex Element of COMPLEX
addcomplex $$ (((y *'),(x *'),((M @) @))) is complex Element of COMPLEX
(((y *'),(x *'),M)) is complex Element of COMPLEX
(((y *'),(x *'),M)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum (((y *'),(x *'),M)) is complex Element of COMPLEX
addcomplex $$ (((y *'),(x *'),M)) is complex Element of COMPLEX
((y *'),(x *'),M) @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((((y *'),(x *'),M) @)) is complex Element of COMPLEX
((((y *'),(x *'),M) @)) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((((y *'),(x *'),M) @)) is complex Element of COMPLEX
addcomplex $$ ((((y *'),(x *'),M) @)) is complex Element of COMPLEX
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x *'),(y *'),(M)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(((x *'),(y *'),(M))) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((((x *'),(y *'),(M)))) is complex Element of COMPLEX
((((x *'),(y *'),(M)))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((((x *'),(y *'),(M)))) is complex Element of COMPLEX
addcomplex $$ ((((x *'),(y *'),(M)))) is complex Element of COMPLEX
((x,y,(M @))) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
(((x,y,(M @)))) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((((x,y,(M @))))) is complex Element of COMPLEX
((((x,y,(M @))))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((((x,y,(M @))))) is complex Element of COMPLEX
addcomplex $$ ((((x,y,(M @))))) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M,x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|((M,x),y)| is complex Element of COMPLEX
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
M @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M),y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|(x,((M),y))| is complex Element of COMPLEX
(x,y,(M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((x,y,(M @))) is complex Element of COMPLEX
((x,y,(M @))) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
Sum ((x,y,(M @))) is complex Element of COMPLEX
addcomplex $$ ((x,y,(M @))) is complex Element of COMPLEX
x is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
y is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
len y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
M is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
len M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width M is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
(M,y) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|(x,(M,y))| is complex Element of COMPLEX
(M) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
M @ is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M @)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *
((M),x) is V1() V4( NAT ) V5( COMPLEX ) Function-like FinSequence-like complex-yielding FinSequence of COMPLEX
|(((M),x),y)| is complex Element of COMPLEX
len ((M),x) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M @) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (M,y) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
|((M,y),x)| is complex Element of COMPLEX
|((M,y),x)| *' is complex Element of COMPLEX
|(y,((M),x))| is complex Element of COMPLEX
|(y,((M),x))| *' is complex Element of COMPLEX