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
[:COMPLEX,COMPLEX:] is non trivial V28() complex-yielding set
bool [:COMPLEX,COMPLEX:] is non trivial V28() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial V28() complex-yielding set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non trivial V28() set
[:REAL,REAL:] is non trivial V28() complex-yielding V159() V160() set
bool [:REAL,REAL:] is non trivial V28() set
[:[:REAL,REAL:],REAL:] is non trivial V28() complex-yielding V159() V160() set
bool [:[:REAL,REAL:],REAL:] is non trivial V28() set
[:RAT,RAT:] is V5( RAT ) non trivial V28() complex-yielding V159() V160() set
bool [:RAT,RAT:] is non trivial V28() set
[:[:RAT,RAT:],RAT:] is V5( RAT ) non trivial V28() complex-yielding V159() V160() set
bool [:[:RAT,RAT:],RAT:] is non trivial V28() set
[:INT,INT:] is V5( RAT ) V5( INT ) non trivial V28() complex-yielding V159() V160() set
bool [:INT,INT:] is non trivial V28() set
[:[:INT,INT:],INT:] is V5( RAT ) V5( INT ) non trivial V28() complex-yielding V159() V160() set
bool [:[:INT,INT:],INT:] is non trivial V28() set
[:NAT,NAT:] is V5( RAT ) V5( INT ) complex-yielding V159() V160() V161() set
[:[:NAT,NAT:],NAT:] is V5( RAT ) V5( INT ) complex-yielding V159() V160() V161() set
bool [:[:NAT,NAT:],NAT:] is 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
F_Real is non empty V44() non trivial right_complementable almost_left_invertible strict unital associative commutative V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
K208() is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like quasi_total complex-yielding V159() V160() Element of bool [:[:REAL,REAL:],REAL:]
K210() is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like quasi_total complex-yielding V159() V160() Element of bool [:[:REAL,REAL:],REAL:]
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
REAL * is functional non empty FinSequence-membered FinSequenceSet of 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 (TOP-REAL 2) 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
n is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() 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
A is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of 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
n - A is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of REAL
K475(A) is V1() Function-like complex-yielding set
- 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
x0 -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
B is V1() V4( NAT ) V5( REAL ) Function-like V28() V35(x0) FinSequence-like FinSubsequence-like complex-yielding V159() V160() Element of x0 -tuples_on REAL
i4 is V1() V4( NAT ) V5( REAL ) Function-like V28() V35(x0) FinSequence-like FinSubsequence-like complex-yielding V159() V160() Element of x0 -tuples_on REAL
B - i4 is V1() V4( NAT ) V5( REAL ) Function-like V28() V35(x0) FinSequence-like FinSubsequence-like complex-yielding V159() V160() Element of x0 -tuples_on REAL
K475(i4) is V1() Function-like complex-yielding set
(- 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
n is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() 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
A is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of 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
n + A is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of REAL
0* (len n) is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() Element of REAL (len n)
REAL (len n) is functional FinSequence-membered FinSequenceSet of REAL
- A is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of REAL
- 1 is V90() set
(- 1) * A is V1() Function-like set
- n is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of REAL
(- 1) * n is V1() Function-like set
(0* (len n)) - A is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of REAL
K475(A) is V1() Function-like complex-yielding set
K446((0* (len n)),K475(A)) is V1() Function-like set
- (- A) is V1() V4( NAT ) V5( REAL ) Function-like V28() FinSequence-like FinSubsequence-like complex-yielding V159() V160() FinSequence of REAL
(- 1) * (- A) is V1() Function-like set
n is non empty set
n * is functional non empty FinSequence-membered FinSequenceSet of n
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 V1() V4( NAT ) V5(n * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of n *
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 (width y) -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
(width y) -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n
y . A is FinSequence-like set
dom y is V28() V168() V169() V170() V171() V172() V173() Element of bool NAT
n is non empty set
n * is functional non empty FinSequence-membered FinSequenceSet of n
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 is V1() V4( NAT ) V5(n * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of n *
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
B is V1() V4( NAT ) V5(n) Function-like V28() FinSequence-like FinSubsequence-like FinSequence 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
x0 is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
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 is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(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)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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
A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of n,n, REAL
y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of n,n, REAL
A * y 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 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) * (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 *
MXF2MXR ((MXR2MXF A) * (MXR2MXF y)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 (MXR2MXF A) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (MXR2MXF y) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (MXR2MXF A) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
len (MXR2MXF 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 real set
A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n * A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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
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 * (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 (y * (MXR2MXF A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXR2MXF (MXF2MXR (y * (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 *
width (MXR2MXF (MXF2MXR (y * (MXR2MXF A)))) 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 * (MXR2MXF A)))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
n 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
A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 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
n - A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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 *
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) - (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) - (MXR2MXF A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 (width n) 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 (width n)):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
- (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) + (- (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) + (- (MXR2MXF A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (MXF2MXR ((MXR2MXF n) + (- (MXR2MXF A)))) is ordinal natural V28() V33() V90() real V92() V93() ext-real non negative V168() V169() V170() V171() V172() V173() Element of NAT
width (MXF2MXR ((MXR2MXF n) + (- (MXR2MXF 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 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
A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of n,n, REAL
y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular Matrix of n,n, REAL
A * y 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 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) * (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 *
MXF2MXR ((MXR2MXF A) * (MXR2MXF y)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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
n 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
A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 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
A - 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) - (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 A) - (MXR2MXF A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n + (A - A) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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 *
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 n) + (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 n) + (MXR2MXF (A - A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0_Rmatrix ((len A),(width A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,(len A),(width 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
MXF2MXR (0. (F_Real,(len A),(width A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n + (0_Rmatrix ((len A),(width A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXR2MXF (0_Rmatrix ((len A),(width 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) + (MXR2MXF (0_Rmatrix ((len A),(width 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) + (MXR2MXF (0_Rmatrix ((len A),(width A))))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXF2MXR (MXR2MXF n) 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) + (- (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 A) + (- (MXR2MXF A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(MXF2MXR (MXR2MXF n)) + (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF A)))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
MXR2MXF (MXF2MXR (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 (MXF2MXR ((MXR2MXF 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 *
(MXR2MXF (MXF2MXR (MXR2MXF n))) + (MXR2MXF (MXF2MXR ((MXR2MXF 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 (MXF2MXR (MXR2MXF n))) + (MXR2MXF (MXF2MXR ((MXR2MXF A) + (- (MXR2MXF A)))))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n 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
A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 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
n + A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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 *
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) + (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) + (MXR2MXF A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n + A) - A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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)) - (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 *
- 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 *
MXF2MXR (- (MXR2MXF A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n + A) + (- 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 (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 *
A + (- A) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(MXR2MXF 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 A) + (MXR2MXF (- A))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n + (A + (- A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 n) + (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 n) + (MXR2MXF (A + (- A)))) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
A - A is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(MXR2MXF 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 A) - (MXR2MXF A)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n + (A - A) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 n) + (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 n) + (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
y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
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 (width y) 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 (width y)):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
- y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 *
- (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 *
MXF2MXR (- (MXR2MXF y)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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
(MXR2MXF y) * (n,A) is V90() real ext-real Element of the U1 of F_Real
- ((MXR2MXF y) * (n,A)) is V90() real ext-real Element of the U1 of F_Real
K182(((MXR2MXF y) * (n,A))) is V90() real ext-real Element of REAL
- 1 is V90() real ext-real Element of REAL
n is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(- 1) * n is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
- n is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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 *
- (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 *
MXF2MXR (- (MXR2MXF n)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 (width n) 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 (width n)):] 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
n is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
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 (width n) 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 (width n)):] is V5( INT ) V5( RAT ) V28() complex-yielding V159() V160() V161() set
- n is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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 *
- (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 *
MXF2MXR (- (MXR2MXF n)) is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of 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 is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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
y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n * A) * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
A * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n * (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 * (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 (width y) 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 (width 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
(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
y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n + A) * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
A * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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 (width y) 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 (width y)):] 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
y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n - A) * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
A * y is V1() V4( NAT ) V5(REAL * ) Function-like V28() FinSequence-like FinSubsequence-like tabular FinSequence 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 (width y) 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 (width y)):] 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
A is non empty V44() non trivial right_complementable almost_left_invertible unital associative commutative V122() V123() V124() right-distributive left-distributive right_unital well-unital V136() left_unital doubleLoopStr
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,(width y)) 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()