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

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

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

RAT is non zero V33() V162() V163() V164() V165() V168() set
INT is non zero V33() V162() V163() V164() V165() V166() V168() set

is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

0 is Function-like functional zero V162() V163() V164() V165() V166() V167() V168() set

1 / 2 is non zero V52() complex ext-real V161() Element of RAT

(1 / 2) * <i> is complex Element of COMPLEX
- ((1 / 2) * <i>) 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
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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg ()):] 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
width y is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg ()):] 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,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

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

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,j] is set
Indices y is set
dom y is V162() V163() V164() V165() V166() V167() Element of bool NAT
Seg () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg ()):] 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

len y 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
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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg ()):] 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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() 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,y] is 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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg ()):] 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 ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set
x is complex set

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 * () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (M * ())) 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 * ()))) 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 () 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 * ()))) 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 () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

[x,y] is set
M is complex set

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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

(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 * (x,y) is complex Element of COMPLEX
() * (x,y) is complex Element of the U1 of F_Complex
Indices () is set
dom () is V162() V163() V164() V165() V166() V167() Element of bool NAT
width () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ()),(Seg ()):] 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 * () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (i9 * ())) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

j9 * (x,y) is complex Element of COMPLEX
(i9 * ()) * (x,y) is complex Element of the U1 of F_Complex
i9 * (() * (x,y)) is complex Element of the U1 of F_Complex
i9 * (() * (x,y)) is complex Element of COMPLEX
M * (() * (x,y)) is complex Element of COMPLEX
x is complex set

((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,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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg ()):] 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

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

(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

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 *
() + () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (() + ())) 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 (() + ()))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (() + ()) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width () 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 (() + ()))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (() + ()) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

[x,y] is 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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

(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 *
() + () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (() + ())) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

j * (x,y) is complex Element of COMPLEX
() * (x,y) is complex Element of the U1 of F_Complex
Indices () is set
dom () is V162() V163() V164() V165() V166() V167() Element of bool NAT
width () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ()),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

i9 * (x,y) is complex Element of COMPLEX
() * (x,y) is complex Element of the U1 of F_Complex

n3 * (x,y) is complex Element of COMPLEX
(COMPLEX2Field (M + i)) * (x,y) is complex Element of the U1 of F_Complex
(() * (x,y)) + (() * (x,y)) is complex Element of the U1 of F_Complex
(() * (x,y)) + (() * (x,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

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 *

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,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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg ()):] 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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg ()):] 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

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 *
- () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (- ())) 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 (- ()))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (- ()) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width () 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 (- ()))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (- ()) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

[x,y] is 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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

(- 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 *
- () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (- ())) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

j * (x,y) is complex Element of COMPLEX
() * (x,y) is complex Element of the U1 of F_Complex
Indices () is set
dom () is V162() V163() V164() V165() V166() V167() Element of bool NAT
width () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ()),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

i * (x,y) is complex Element of COMPLEX
(- ()) * (x,y) is complex Element of the U1 of F_Complex
- (() * (x,y)) is complex Element of the U1 of F_Complex
- 1 is non zero V52() V107() complex ext-real V161() Element of INT

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,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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg ()):] 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

(((- 1) * x)) is V1() V4( NAT ) V5(COMPLEX * ) Function-like FinSequence-like tabular FinSequence of COMPLEX *

() *' is complex Element of COMPLEX
(() *') * (x) 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 *
() - () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (() - ())) 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 (() - ()))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width (() - ()) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
- () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
() + (- ()) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
width (() + (- ())) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
width () 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 (() - ()))) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (() - ()) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len (() + (- ())) is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
len () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

[x,y] is set

len M 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 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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom M),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

(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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom i),(Seg ()):] 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 () is set
dom () is V162() V163() V164() V165() V166() V167() Element of bool NAT
width () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ()),(Seg ()):] 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 *
() - () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

COMPLEX2Field (Field2COMPLEX (() - ())) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *

i9 * (x,y) is complex Element of COMPLEX
() * (x,y) is complex Element of the U1 of F_Complex
Indices () is set
dom () is V162() V163() V164() V165() V166() V167() Element of bool NAT
width () is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT
Seg () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom ()),(Seg ()):] is V5( RAT ) V5( INT ) complex-yielding V152() V153() V154() set

j * (x,y) is complex Element of COMPLEX
() * (x,y) is complex Element of the U1 of F_Complex
- (i * (x,y)) is complex Element of COMPLEX
- (() * (x,y)) is complex Element of the U1 of F_Complex

n3 * (x,y) is complex Element of COMPLEX
(COMPLEX2Field (M - i)) * (x,y) is complex Element of the U1 of F_Complex
- () is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
() + (- ()) is V1() V4( NAT ) V5( the U1 of F_Complex * ) Function-like FinSequence-like tabular FinSequence of the U1 of F_Complex *
(() + (- ())) * (x,y) is complex Element of the U1 of F_Complex
(- ()) * (x,y) is complex Element of the U1 of F_Complex
(() * (x,y)) + ((- ()) * (x,y)) is complex Element of the U1 of F_Complex
(() * (x,y)) + ((- ()) * (x,y)) is complex Element of COMPLEX
(() * (x,y)) + (- (() * (x,y))) is complex Element of the U1 of F_Complex
(() * (x,y)) + (- (() * (x,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

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 *

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,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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom x),(Seg ()):] 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 () is V162() V163() V164() V165() V166() V167() Element of bool NAT
[:(dom y),(Seg ()):] 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

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

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

len <*(x . i9)*> is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

rng i is functional Element of bool ()
bool () is set

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

i . i9 is V1() Function-like set
x . i9 is complex Element 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

width j is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

i . i9 is V1() Function-like set
x . i9 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
width y 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
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

y . i is V1() Function-like set
x . i is complex Element of COMPLEX

M . i is V1() Function-like set

len x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

rng j is V162() Element of bool COMPLEX

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

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

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

M . i is complex Element of COMPLEX

width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

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

len M 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
dom M is V162() V163() V164() V165() V166() V167() Element of bool NAT

M . j is complex Element of COMPLEX

width x is ordinal natural V52() V107() complex ext-real non negative V161() V162() V163() V164() V165() V166() V167() Element of NAT

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