:: MATRIXR2 semantic presentation

REAL is non empty non trivial V28() V168() V169() V170() V174() set
NAT is non trivial ordinal V28() V33() V34() V168() V169() V170() V171() V172() V173() V174() Element of bool REAL
bool REAL is non trivial V28() set
INT is non empty non trivial V28() V168() V169() V170() V171() V172() V174() set
omega is non trivial ordinal V28() V33() V34() V168() V169() V170() V171() V172() V173() V174() set
bool omega is non trivial V28() set
bool NAT is non trivial V28() set
COMPLEX is non empty non trivial V28() V168() V174() set
RAT is non empty non trivial V28() V168() V169() V170() V171() V174() set

bool is non trivial V28() set

bool is non trivial V28() set
is non trivial V28() complex-yielding V159() V160() set
bool is non trivial V28() set
is non trivial V28() complex-yielding V159() V160() set
bool is non trivial V28() set
is V5( RAT ) non trivial V28() complex-yielding V159() V160() set
bool is non trivial V28() set
is V5( RAT ) non trivial V28() complex-yielding V159() V160() set
bool is non trivial V28() set
is V5( RAT ) V5( INT ) non trivial V28() complex-yielding V159() V160() set
bool is non trivial V28() set
is V5( RAT ) V5( INT ) non trivial V28() complex-yielding V159() V160() set
bool is non trivial V28() set
is V5( RAT ) V5( INT ) complex-yielding V159() V160() V161() set

{} is functional empty ordinal natural V28() V32() V33() V35( {} ) FinSequence-membered ext-real non positive non negative V168() V169() V170() V171() V172() V173() V174() set
K271(NAT) is V100() set
1 is non empty ordinal natural V28() V33() V90() real V92() V93() ext-real positive non negative V168() V169() V170() V171() V172() V173() Element of NAT
2 is non empty ordinal natural V28() V33() V90() real V92() V93() ext-real positive non negative V168() V169() V170() V171() V172() V173() Element of NAT

0 is functional empty ordinal natural V28() V32() V33() V35( {} ) FinSequence-membered V90() real V92() V93() ext-real non positive non negative V168() V169() V170() V171() V172() V173() V174() Element of NAT
doubleLoopStr(# REAL,K208(),K210(),1,0 #) is strict doubleLoopStr
the U1 of F_Real is non empty non trivial V168() V169() V170() set
the U1 of F_Real * is functional non empty FinSequence-membered FinSequenceSet of the U1 of F_Real

[:1,1:] is V5( RAT ) V5( INT ) V28() complex-yielding V159() V160() V161() set
bool [:1,1:] is V28() V32() set
[:[:1,1:],1:] is V5( RAT ) V5( INT ) V28() complex-yielding V159() V160() V161() set
bool [:[:1,1:],1:] is V28() V32() set
[:[:1,1:],REAL:] is complex-yielding V159() V160() set
bool [:[:1,1:],REAL:] is set
[:2,2:] is V5( RAT ) V5( INT ) V28() complex-yielding V159() V160() V161() set
[:[:2,2:],REAL:] is complex-yielding V159() V160() set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is V210() L16()
the U1 of () is set
3 is non empty ordinal natural V28() V33() V90() real V92() V93() ext-real positive non negative V168() V169() V170() V171() V172() V173() Element of NAT
Seg 3 is non empty V28() V35(3) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
{1,2,3} is V28() V168() V169() V170() V171() V172() V173() set

len n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

- 1 is V90() set
(- 1) * A is V1() Function-like set
K446(n,K475(A)) is V1() Function-like set
y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
(n - A) . y is V90() real ext-real set
n . y is V90() real ext-real set
A . y is V90() real ext-real set
(n . y) - (A . y) is set
x0 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

(- 1) * i4 is V1() Function-like set
K446(B,K475(i4)) is V1() Function-like set
(B - i4) . y is V90() real ext-real set
B . y is V90() real ext-real set
i4 . y is V90() real ext-real set
(B . y) - (i4 . y) is set

len n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

- 1 is V90() set
(- 1) * A is V1() Function-like set

(- 1) * n is V1() Function-like set

K446((0* (len n)),K475(A)) is V1() Function-like set

(- 1) * (- A) is V1() Function-like set
n is non empty set

A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Line (y,A) is V1() V4( NAT ) V5(n) Function-like V28() V35( width y) FinSequence-like FinSubsequence-like Element of () -tuples_on n
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

dom y is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
n is non empty set

A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

x0 . A is FinSequence-like set
len x0 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width x0 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
x0 * (A,y) is Element of n

len B is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
B . y is set
Seg (width x0) is V28() V35( width x0) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width x0 ) } is set
dom B is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
rng B is V28() set
i4 is Element of n
dom x0 is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
[A,y] is set
{A,y} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{A} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{A,y},{A}} is non empty V28() V32() set
Indices x0 is set
[:(dom x0),(Seg (width x0)):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
[n,A] is set
{n,A} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{n} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{n,A},{n}} is non empty V28() V32() set
y is real set

Indices x0 is set
dom x0 is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
width x0 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Seg (width x0) is V28() V35( width x0) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width x0 ) } is set
[:(dom x0),(Seg (width x0)):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set

(y * x0) * (n,A) is V90() real ext-real Element of REAL
x0 * (n,A) is V90() real ext-real Element of REAL
y * (x0 * (n,A)) is V90() real ext-real Element of REAL
MXR2MXF x0 is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
B is V90() real ext-real Element of the U1 of F_Real
B * (MXR2MXF x0) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

(MXF2MXR (B * (MXR2MXF x0))) * (n,A) is V90() real ext-real Element of REAL
(MXR2MXF x0) * (n,A) is V90() real ext-real Element of the U1 of F_Real
B * ((MXR2MXF x0) * (n,A)) is V90() real ext-real Element of the U1 of F_Real
K186(B,((MXR2MXF x0) * (n,A))) is V90() real ext-real Element of REAL
n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

MXR2MXF A is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF y is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() * () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

len (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width () is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len () is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width () is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len () is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
n is real set

len (n * A) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (n * A) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
MXR2MXF A is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
y is V90() real ext-real Element of the U1 of F_Real
y * () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

MXR2MXF (MXF2MXR (y * ())) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
width (MXR2MXF (MXF2MXR (y * ()))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (MXR2MXF (MXF2MXR (y * ()))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

MXR2MXF n is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF A is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() - () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

len (n - A) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (n - A) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Indices n is set
dom n is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg () is V28() V35( width n) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width n ) } is set
[:(dom n),(Seg ()):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
- () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() + (- ()) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

len (MXF2MXR (() + (- ()))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (MXF2MXR (() + (- ()))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
x0 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
[y,x0] is set
{y,x0} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{y} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{y,x0},{y}} is non empty V28() V32() set
(n - A) * (y,x0) is V90() real ext-real Element of REAL
n * (y,x0) is V90() real ext-real Element of REAL
A * (y,x0) is V90() real ext-real Element of REAL
(n * (y,x0)) - (A * (y,x0)) is V90() real ext-real Element of REAL
n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

MXR2MXF A is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF y is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() * () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

MXR2MXF A is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() - () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

MXR2MXF n is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF (A - A) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() + (MXR2MXF (A - A)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR (() + (MXR2MXF (A - A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *

0. (F_Real,(len A),()) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of len A, width A, the U1 of F_Real

n + (0_Rmatrix ((len A),())) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXR2MXF (0_Rmatrix ((len A),())) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() + (MXR2MXF (0_Rmatrix ((len A),()))) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR (() + (MXR2MXF (0_Rmatrix ((len A),())))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *

- () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() + (- ()) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

(MXF2MXR ()) + (MXF2MXR (() + (- ()))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXR2MXF (MXF2MXR ()) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF (MXF2MXR (() + (- ()))) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
(MXR2MXF (MXF2MXR ())) + (MXR2MXF (MXF2MXR (() + (- ())))) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR ((MXR2MXF (MXF2MXR ())) + (MXR2MXF (MXF2MXR (() + (- ()))))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *

len n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

len A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

MXR2MXF n is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF A is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() + () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

MXR2MXF (n + A) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
(MXR2MXF (n + A)) - () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR ((MXR2MXF (n + A)) - ()) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *

- () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

MXR2MXF (- A) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
(MXR2MXF (n + A)) + (MXR2MXF (- A)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR ((MXR2MXF (n + A)) + (MXR2MXF (- A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *

() + (MXR2MXF (- A)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

MXR2MXF (A + (- A)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() + (MXR2MXF (A + (- A))) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR (() + (MXR2MXF (A + (- A)))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *

() - () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

MXR2MXF (A - A) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
() + (MXR2MXF (A - A)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR (() + (MXR2MXF (A - A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
[n,A] is set
{n,A} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{n} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{n,A},{n}} is non empty V28() V32() set

Indices y is set
dom y is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Seg () is V28() V35( width y) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width y ) } is set
[:(dom y),(Seg ()):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set

MXR2MXF y is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
- () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

(- y) * (n,A) is V90() real ext-real Element of REAL
y * (n,A) is V90() real ext-real Element of REAL
- (y * (n,A)) is V90() real ext-real Element of REAL
() * (n,A) is V90() real ext-real Element of the U1 of F_Real
- (() * (n,A)) is V90() real ext-real Element of the U1 of F_Real
K182((() * (n,A))) is V90() real ext-real Element of REAL
- 1 is V90() real ext-real Element of REAL

MXR2MXF n is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
- () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

width ((- 1) * n) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len ((- 1) * n) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
A is ordinal natural V28() V33() ext-real non negative set
y is ordinal natural V28() V33() ext-real non negative set
[A,y] is set
{A,y} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{A} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{A,y},{A}} is non empty V28() V32() set
Indices ((- 1) * n) is set
dom ((- 1) * n) is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg (width ((- 1) * n)) is V28() V35( width ((- 1) * n)) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width ((- 1) * n) ) } is set
[:(dom ((- 1) * n)),(Seg (width ((- 1) * n))):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
B is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
x0 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
[x0,B] is set
{x0,B} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{x0} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{x0,B},{x0}} is non empty V28() V32() set
Indices n is set
dom n is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg () is V28() V35( width n) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width n ) } is set
[:(dom n),(Seg ()):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
((- 1) * n) * (A,y) is V90() real ext-real Element of REAL
n * (x0,B) is V90() real ext-real Element of REAL
(- 1) * (n * (x0,B)) is V90() real ext-real Element of REAL
n * (A,y) is V90() real ext-real Element of REAL
- (n * (A,y)) is V90() real ext-real Element of REAL
(- n) * (A,y) is V90() real ext-real Element of REAL
len (- n) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (- n) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

Indices n is set
dom n is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
width n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Seg () is V28() V35( width n) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width n ) } is set
[:(dom n),(Seg ()):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set

MXR2MXF n is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
- () is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *

A is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
[A,y] is set
{A,y} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{A} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{A,y},{A}} is non empty V28() V32() set
(- n) * (A,y) is V90() real ext-real Element of REAL
n * (A,y) is V90() real ext-real Element of REAL
- (n * (A,y)) is V90() real ext-real Element of REAL

(- 1) * (n * (A,y)) is V90() real ext-real Element of REAL
n is V90() real ext-real Element of REAL
A is V90() real ext-real Element of REAL
n * A is V90() real ext-real Element of REAL

len ((n * A) * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width ((n * A) * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (n * (A * y)) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (n * (A * y)) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Indices (n * (A * y)) is set
dom (n * (A * y)) is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg (width (n * (A * y))) is V28() V35( width (n * (A * y))) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width (n * (A * y)) ) } is set
[:(dom (n * (A * y))),(Seg (width (n * (A * y)))):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
x0 is ordinal natural V28() V33() ext-real non negative set
B is ordinal natural V28() V33() ext-real non negative set
[x0,B] is set
{x0,B} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{x0} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{x0,B},{x0}} is non empty V28() V32() set
(n * (A * y)) * (x0,B) is V90() real ext-real Element of REAL
((n * A) * y) * (x0,B) is V90() real ext-real Element of REAL
Indices (A * y) is set
dom (A * y) is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg (width (A * y)) is V28() V35( width (A * y)) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width (A * y) ) } is set
[:(dom (A * y)),(Seg (width (A * y))):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
Indices y is set
dom y is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg () is V28() V35( width y) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width y ) } is set
[:(dom y),(Seg ()):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
i4 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
j4 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
(A * y) * (i4,j4) is V90() real ext-real Element of REAL
n * ((A * y) * (i4,j4)) is V90() real ext-real Element of REAL
y * (i4,j4) is V90() real ext-real Element of REAL
A * (y * (i4,j4)) is V90() real ext-real Element of REAL
n * (A * (y * (i4,j4))) is V90() real ext-real Element of REAL
(n * A) * (y * (i4,j4)) is V90() real ext-real Element of REAL
n is V90() real ext-real Element of REAL
A is V90() real ext-real Element of REAL
n + A is V90() real ext-real Element of REAL

(n * y) + (A * y) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXR2MXF (n * y) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF (A * y) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
(MXR2MXF (n * y)) + (MXR2MXF (A * y)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR ((MXR2MXF (n * y)) + (MXR2MXF (A * y))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (n * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (n * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len ((n + A) * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width ((n + A) * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Indices ((n + A) * y) is set
dom ((n + A) * y) is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg (width ((n + A) * y)) is V28() V35( width ((n + A) * y)) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width ((n + A) * y) ) } is set
[:(dom ((n + A) * y)),(Seg (width ((n + A) * y))):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
x0 is ordinal natural V28() V33() ext-real non negative set
B is ordinal natural V28() V33() ext-real non negative set
[x0,B] is set
{x0,B} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{x0} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{x0,B},{x0}} is non empty V28() V32() set
((n + A) * y) * (x0,B) is V90() real ext-real Element of REAL
((n * y) + (A * y)) * (x0,B) is V90() real ext-real Element of REAL
Indices y is set
dom y is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg () is V28() V35( width y) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width y ) } is set
[:(dom y),(Seg ()):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
Indices (n * y) is set
dom (n * y) is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg (width (n * y)) is V28() V35( width (n * y)) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width (n * y) ) } is set
[:(dom (n * y)),(Seg (width (n * y))):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
i4 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
j4 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
(n * y) * (i4,j4) is V90() real ext-real Element of REAL
(A * y) * (i4,j4) is V90() real ext-real Element of REAL
((n * y) * (i4,j4)) + ((A * y) * (i4,j4)) is V90() real ext-real Element of REAL
y * (i4,j4) is V90() real ext-real Element of REAL
n * (y * (i4,j4)) is V90() real ext-real Element of REAL
(n * (y * (i4,j4))) + ((A * y) * (i4,j4)) is V90() real ext-real Element of REAL
A * (y * (i4,j4)) is V90() real ext-real Element of REAL
(n * (y * (i4,j4))) + (A * (y * (i4,j4))) is V90() real ext-real Element of REAL
y * (x0,B) is V90() real ext-real Element of REAL
(n + A) * (y * (x0,B)) is V90() real ext-real Element of REAL
len ((n * y) + (A * y)) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width ((n * y) + (A * y)) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
n is V90() real ext-real Element of REAL
A is V90() real ext-real Element of REAL
n - A is V90() real ext-real Element of REAL

(n * y) - (A * y) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXR2MXF (n * y) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXR2MXF (A * y) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
(MXR2MXF (n * y)) - (MXR2MXF (A * y)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR ((MXR2MXF (n * y)) - (MXR2MXF (A * y))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len ((n - A) * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width ((n - A) * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (n * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (n * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (A * y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
Indices ((n - A) * y) is set
dom ((n - A) * y) is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg (width ((n - A) * y)) is V28() V35( width ((n - A) * y)) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width ((n - A) * y) ) } is set
[:(dom ((n - A) * y)),(Seg (width ((n - A) * y))):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
x0 is ordinal natural V28() V33() ext-real non negative set
B is ordinal natural V28() V33() ext-real non negative set
[x0,B] is set
{x0,B} is non empty V28() V32() V168() V169() V170() V171() V172() V173() set
{x0} is non empty trivial V28() V32() V35(1) V168() V169() V170() V171() V172() V173() set
{{x0,B},{x0}} is non empty V28() V32() set
((n - A) * y) * (x0,B) is V90() real ext-real Element of REAL
((n * y) - (A * y)) * (x0,B) is V90() real ext-real Element of REAL
Indices y is set
dom y is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg () is V28() V35( width y) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width y ) } is set
[:(dom y),(Seg ()):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
Indices (n * y) is set
dom (n * y) is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
Seg (width (n * y)) is V28() V35( width (n * y)) V168() V169() V170() V171() V172() V173() Element of bool NAT
{ b1 where b1 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT : ( 1 <= b1 & b1 <= width (n * y) ) } is set
[:(dom (n * y)),(Seg (width (n * y))):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
i4 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
j4 is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
(n * y) * (i4,j4) is V90() real ext-real Element of REAL
(A * y) * (i4,j4) is V90() real ext-real Element of REAL
((n * y) * (i4,j4)) - ((A * y) * (i4,j4)) is V90() real ext-real Element of REAL
y * (i4,j4) is V90() real ext-real Element of REAL
n * (y * (i4,j4)) is V90() real ext-real Element of REAL
(n * (y * (i4,j4))) - ((A * y) * (i4,j4)) is V90() real ext-real Element of REAL
A * (y * (i4,j4)) is V90() real ext-real Element of REAL
(n * (y * (i4,j4))) - (A * (y * (i4,j4))) is V90() real ext-real Element of REAL
y * (x0,B) is V90() real ext-real Element of REAL
(n - A) * (y * (x0,B)) is V90() real ext-real Element of REAL
width ((n * y) - (A * y)) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
- (MXR2MXF (A * y)) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
(MXR2MXF (n * y)) + (- (MXR2MXF (A * y))) is V1() V4( NAT ) V5( the U1 of F_Real * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of F_Real *
MXF2MXR ((MXR2MXF (n * y)) + (- (MXR2MXF (A * y)))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width (MXF2MXR ((MXR2MXF (n * y)) + (- (MXR2MXF (A * y))))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len ((n * y) - (A * y)) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (MXF2MXR ((MXR2MXF (n * y)) + (- (MXR2MXF (A * y))))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
n is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT

the U1 of A is non empty non trivial set
the U1 of A * is functional non empty FinSequence-membered FinSequenceSet of the U1 of A
y is V1() V4( NAT ) V5( the U1 of A * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of A *
len y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
0. (A,n,(len y)) is V1() V4( NAT ) V5( the U1 of A * ) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of n, len y, the U1 of A
(0. (A,n,(len y))) * y is V1() V4( NAT ) V5( the U1 of A * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of the U1 of A *
width y is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
0. (A,n,()) is V1() V4( NAT ) V5( the U1 of A * ) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of n, width y, the U1 of A
len (0. (A,n,(len y))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171()