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