:: MATRIXR1 semantic presentation

REAL is V1() V32() V145() V146() V147() V151() set
NAT is V145() V146() V147() V148() V149() V150() V151() Element of K6(REAL)
K6(REAL) is set
INT is V1() V32() V145() V146() V147() V148() V149() V151() set
COMPLEX is V1() V32() V145() V151() set
RAT is V1() V32() V145() V146() V147() V148() V151() set
K7(COMPLEX,COMPLEX) is complex-yielding set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is complex-yielding set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is complex-yielding V109() V110() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is complex-yielding V109() V110() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V17( RAT ) complex-yielding V109() V110() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V17( RAT ) complex-yielding V109() V110() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V17( RAT ) V17( INT ) complex-yielding V109() V110() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V17( RAT ) V17( INT ) complex-yielding V109() V110() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V17( RAT ) V17( INT ) complex-yielding V109() V110() V111() set
K7(K7(NAT,NAT),NAT) is V17( RAT ) V17( INT ) complex-yielding V109() V110() V111() set
K6(K7(K7(NAT,NAT),NAT)) is set
omega is V145() V146() V147() V148() V149() V150() V151() set
K6(omega) is set
K6(NAT) is set
1 is V1() ordinal natural V11() real V30() V31() ext-real positive non negative V145() V146() V147() V148() V149() V150() Element of NAT
K7(1,1) is V17( RAT ) V17( INT ) complex-yielding V109() V110() V111() set
K6(K7(1,1)) is set
K7(K7(1,1),1) is V17( RAT ) V17( INT ) complex-yielding V109() V110() V111() set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is complex-yielding V109() V110() set
K6(K7(K7(1,1),REAL)) is set
2 is V1() ordinal natural V11() real V30() V31() ext-real positive non negative V145() V146() V147() V148() V149() V150() Element of NAT
K7(2,2) is V17( RAT ) V17( INT ) complex-yielding V109() V110() V111() set
K7(K7(2,2),REAL) is complex-yielding V109() V110() set
K6(K7(K7(2,2),REAL)) is set
TOP-REAL 2 is V160() L15()
the carrier of (TOP-REAL 2) is set
the carrier of (TOP-REAL 2) * is V1() functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
0 is V1() functional FinSequence-membered V145() V146() V147() V148() V149() V150() V151() set
3 is V1() ordinal natural V11() real V30() V31() ext-real positive non negative V145() V146() V147() V148() V149() V150() Element of NAT
0 is V1() ordinal natural V11() real functional V30() V31() FinSequence-membered ext-real non positive non negative V145() V146() V147() V148() V149() V150() V151() Element of NAT
F_Real is non empty non degenerated V49() right_complementable almost_left_invertible strict V98() V99() V100() unital V191() V193() right-distributive left-distributive right_unital well-unital V199() left_unital doubleLoopStr
K153() is V13() V16(K7(REAL,REAL)) V17( REAL ) Function-like V27(K7(REAL,REAL), REAL ) complex-yielding V109() V110() Element of K6(K7(K7(REAL,REAL),REAL))
K155() is V13() V16(K7(REAL,REAL)) V17( REAL ) Function-like V27(K7(REAL,REAL), REAL ) complex-yielding V109() V110() Element of K6(K7(K7(REAL,REAL),REAL))
doubleLoopStr(# REAL,K153(),K155(),1,0 #) is strict doubleLoopStr
the carrier of F_Real is V1() V2() V145() V146() V147() set
n is V11() real ext-real Element of REAL
x is V11() real ext-real Element of the carrier of F_Real
m is V11() real ext-real Element of REAL
i is V11() real ext-real Element of the carrier of F_Real
n + m is V11() real ext-real Element of REAL
x + i is V11() real ext-real Element of the carrier of F_Real
K129(x,i) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
x is V11() real ext-real Element of the carrier of F_Real
m is V11() real ext-real Element of REAL
i is V11() real ext-real Element of the carrier of F_Real
n * m is V11() real ext-real Element of REAL
x * i is V11() real ext-real Element of the carrier of F_Real
K131(x,i) is V11() real ext-real Element of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
- n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K38(1) is V11() set
K38(1) * n is V13() Function-like set
n + (- n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
0* (len n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of REAL (len n)
REAL (len n) is functional FinSequence-membered FinSequenceSet of REAL
n - n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(n) is V13() Function-like complex-yielding set
K306(n,K335(n)) is V13() Function-like set
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
x is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
- x is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
K38(1) * x is V13() Function-like set
x + (- x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
(len n) |-> 0 is V13() empty-yielding V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * m is V13() Function-like set
K306(n,K335(m)) is V13() Function-like set
- m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n + (- m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
0* (len n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of REAL (len n)
REAL (len n) is functional FinSequence-membered FinSequenceSet of REAL
n - (0* (len n)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335((0* (len n))) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * (0* (len n)) is V13() Function-like set
K306(n,K335((0* (len n)))) is V13() Function-like set
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
x is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
(len n) |-> 0 is V13() empty-yielding V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
x - ((len n) |-> 0) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
K335(((len n) |-> 0)) is V13() Function-like complex-yielding set
K38(1) * ((len n) |-> 0) is V13() Function-like set
K306(x,K335(((len n) |-> 0))) is V13() Function-like set
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
0* (len n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of REAL (len n)
REAL (len n) is functional FinSequence-membered FinSequenceSet of REAL
(0* (len n)) - n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(n) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * n is V13() Function-like set
K306((0* (len n)),K335(n)) is V13() Function-like set
- n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(len n) |-> 0 is V13() empty-yielding V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
x is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
((len n) |-> 0) - x is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
K335(x) is V13() Function-like complex-yielding set
K38(1) * x is V13() Function-like set
K306(((len n) |-> 0),K335(x)) is V13() Function-like set
- x is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
- m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K38(1) is V11() set
K38(1) * m is V13() Function-like set
n - (- m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335((- m)) is V13() Function-like complex-yielding set
K38(1) * (- m) is V13() Function-like set
K306(n,K335((- m))) is V13() Function-like set
n + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * m is V13() Function-like set
K306(n,K335(m)) is V13() Function-like set
- (n - m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K38(1) * (n - m) is V13() Function-like set
m - n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(n) is V13() Function-like complex-yielding set
K38(1) * n is V13() Function-like set
K306(m,K335(n)) is V13() Function-like set
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * m is V13() Function-like set
K306(n,K335(m)) is V13() Function-like set
- (n - m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K38(1) * (n - m) is V13() Function-like set
- n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K38(1) * n is V13() Function-like set
(- n) + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * m is V13() Function-like set
K306(n,K335(m)) is V13() Function-like set
0* (len n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of REAL (len n)
REAL (len n) is functional FinSequence-membered FinSequenceSet of REAL
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
i - j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
K335(j) is V13() Function-like complex-yielding set
K38(1) * j is V13() Function-like set
K306(i,K335(j)) is V13() Function-like set
(len n) |-> 0 is V13() empty-yielding V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * m is V13() Function-like set
K306(n,K335(m)) is V13() Function-like set
(n - m) - x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(x) is V13() Function-like complex-yielding set
K38(1) * x is V13() Function-like set
K306((n - m),K335(x)) is V13() Function-like set
m + x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n - (m + x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335((m + x)) is V13() Function-like complex-yielding set
K38(1) * (m + x) is V13() Function-like set
K306(n,K335((m + x))) is V13() Function-like set
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m - x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(x) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * x is V13() Function-like set
K306(m,K335(x)) is V13() Function-like set
n + (m - x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n + m) - x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K306((n + m),K335(x)) is V13() Function-like set
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m - x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(x) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * x is V13() Function-like set
K306(m,K335(x)) is V13() Function-like set
n - (m - x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335((m - x)) is V13() Function-like complex-yielding set
K38(1) * (m - x) is V13() Function-like set
K306(n,K335((m - x))) is V13() Function-like set
n - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) * m is V13() Function-like set
K306(n,K335(m)) is V13() Function-like set
(n - m) + x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n + m) - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * m is V13() Function-like set
K306((n + m),K335(m)) is V13() Function-like set
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
i + j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
(i + j) - j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
K335(j) is V13() Function-like complex-yielding set
K38(1) * j is V13() Function-like set
K306((i + j),K335(j)) is V13() Function-like set
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n - m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(m) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * m is V13() Function-like set
K306(n,K335(m)) is V13() Function-like set
(n - m) + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
i - j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
K335(j) is V13() Function-like complex-yielding set
K38(1) * j is V13() Function-like set
K306(i,K335(j)) is V13() Function-like set
(i - j) + j is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
n is non empty multMagma
the carrier of n is V1() set
m is V13() V16( NAT ) V17( the carrier of n) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is Element of the carrier of n
x * m is V13() V16( NAT ) V17( the carrier of n) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (x * m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len m) -tuples_on the carrier of n is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
i is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( len m) FinSequence-like FinSubsequence-like Element of (len m) -tuples_on the carrier of n
x * i is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( len m) FinSequence-like FinSubsequence-like Element of (len m) -tuples_on the carrier of n
the carrier of n * is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is V13() V16( NAT ) V17( the carrier of n) Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = len m } is set
j is V13() V16( NAT ) V17( the carrier of n) Function-like V32() FinSequence-like FinSubsequence-like Element of the carrier of n *
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V11() real ext-real Element of REAL
m is V11() real ext-real Element of the carrier of F_Real
x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n * x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
i is V13() V16( NAT ) V17( the carrier of F_Real) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of the carrier of F_Real
m * i is V13() V16( NAT ) V17( the carrier of F_Real) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of the carrier of F_Real
len (n * x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m * i) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
j is ordinal natural ext-real non negative set
(n * x) . j is V11() real ext-real Element of REAL
(m * i) . j is V11() real ext-real Element of REAL
Seg (len i) is V32() V39( len i) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom (m * i) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
i . j is V11() real ext-real Element of REAL
p is V11() real ext-real Element of the carrier of F_Real
m * p is V11() real ext-real Element of the carrier of F_Real
K131(m,p) is V11() real ext-real Element of REAL
n is non empty non degenerated V49() right_complementable almost_left_invertible V98() V99() V100() unital V191() V193() right-distributive left-distributive right_unital well-unital V199() left_unital doubleLoopStr
the carrier of n is V1() V2() set
the carrier of n * is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
m is Element of the carrier of n
x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
m * x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
Indices (m * x) is set
dom (m * x) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (m * x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (m * x)) is V32() V39( width (m * x)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m * x)),(Seg (width (m * x)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices x is set
dom x is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width x) is V32() V39( width x) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom x),(Seg (width x))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
len (m * x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is ordinal natural ext-real non negative set
m is non empty non degenerated V49() right_complementable almost_left_invertible V98() V99() V100() unital V191() V193() right-distributive left-distributive right_unital well-unital V199() left_unital doubleLoopStr
the carrier of m is V1() V2() set
the carrier of m * is V1() functional FinSequence-membered FinSequenceSet of the carrier of m
x is Element of the carrier of m
i is V13() V16( NAT ) V17( the carrier of m * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of m *
width i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x * i is V13() V16( NAT ) V17( the carrier of m * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of m *
Col ((x * i),n) is V13() V16( NAT ) V17( the carrier of m) Function-like V32() V39( len (x * i)) FinSequence-like FinSubsequence-like Element of (len (x * i)) -tuples_on the carrier of m
len (x * i) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x * i)) -tuples_on the carrier of m is V1() functional FinSequence-membered FinSequenceSet of the carrier of m
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Col (i,n) is V13() V16( NAT ) V17( the carrier of m) Function-like V32() V39( len i) FinSequence-like FinSubsequence-like Element of (len i) -tuples_on the carrier of m
(len i) -tuples_on the carrier of m is V1() functional FinSequence-membered FinSequenceSet of the carrier of m
x * (Col (i,n)) is V13() V16( NAT ) V17( the carrier of m) Function-like V32() V39( len i) FinSequence-like FinSubsequence-like Element of (len i) -tuples_on the carrier of m
Seg (len (x * i)) is V32() V39( len (x * i)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom (x * i) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom i is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (x * (Col (i,n))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (Col (i,n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (x * (Col (i,n))) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
j is ordinal natural ext-real non negative set
(x * (Col (i,n))) . j is set
(x * i) * (j,n) is Element of the carrier of m
Seg (width i) is V32() V39( width i) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
[j,n] is set
Indices i is set
K7((dom i),(Seg (width i))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
i * (j,n) is Element of the carrier of m
x * (i * (j,n)) is Element of the carrier of m
(Col (i,n)) . j is set
n is non empty non degenerated V49() right_complementable almost_left_invertible V98() V99() V100() unital V191() V193() right-distributive left-distributive right_unital well-unital V199() left_unital doubleLoopStr
the carrier of n is V1() V2() set
the carrier of n * is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
m is Element of the carrier of n
x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m * x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is ordinal natural ext-real non negative set
Line ((m * x),i) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( width (m * x)) FinSequence-like FinSubsequence-like Element of (width (m * x)) -tuples_on the carrier of n
width (m * x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (m * x)) -tuples_on the carrier of n is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
Line (x,i) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of n
(width x) -tuples_on the carrier of n is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
m * (Line (x,i)) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of n
Seg (width x) is V32() V39( width x) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width (m * x)) is V32() V39( width (m * x)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (m * (Line (x,i))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (Line (x,i)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (m * (Line (x,i))) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
j is ordinal natural ext-real non negative set
(m * (Line (x,i))) . j is set
(m * x) * (i,j) is Element of the carrier of n
dom x is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
[i,j] is set
Indices x is set
K7((dom x),(Seg (width x))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
x * (i,j) is Element of the carrier of n
m * (x * (i,j)) is Element of the carrier of n
(Line (x,i)) . j is set
n is non empty non degenerated V49() right_complementable almost_left_invertible V98() V99() V100() unital V191() V193() right-distributive left-distributive right_unital well-unital V199() left_unital doubleLoopStr
the carrier of n is V1() V2() set
the carrier of n * is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
m is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of len m, width x, the carrier of n
Indices i is set
dom i is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width i) is V32() V39( width i) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom i),(Seg (width i))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is non empty non degenerated V49() right_complementable almost_left_invertible V98() V99() V100() unital V191() V193() right-distributive left-distributive right_unital well-unital V199() left_unital doubleLoopStr
the carrier of n is V1() V2() set
the carrier of n * is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
m is Element of the carrier of n
x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m * i is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
x * (m * i) is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
x * i is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
m * (x * i) is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len (m * (x * i)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (x * i) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (x * i) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m * (x * i)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m * i) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices (m * (x * i)) is set
dom (m * (x * i)) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width (m * (x * i))) is V32() V39( width (m * (x * i))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m * (x * i))),(Seg (width (m * (x * i))))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
q2 is ordinal natural ext-real non negative set
Line (x,q2) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of n
(width x) -tuples_on the carrier of n is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
i is ordinal natural ext-real non negative set
[q2,i] is set
(m * (x * i)) * (q2,i) is Element of the carrier of n
Col ((m * i),i) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( len (m * i)) FinSequence-like FinSubsequence-like Element of (len (m * i)) -tuples_on the carrier of n
len (m * i) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (m * i)) -tuples_on the carrier of n is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
(Line (x,q2)) "*" (Col ((m * i),i)) is Element of the carrier of n
Col (i,i) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( len i) FinSequence-like FinSubsequence-like Element of (len i) -tuples_on the carrier of n
(len i) -tuples_on the carrier of n is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
Seg (width i) is V32() V39( width i) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom (x * i) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Indices (x * i) is set
Seg (width (x * i)) is V32() V39( width (x * i)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (x * i)),(Seg (width (x * i)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
(x * i) * (q2,i) is Element of the carrier of n
m * ((x * i) * (q2,i)) is Element of the carrier of n
(Line (x,q2)) "*" (Col (i,i)) is Element of the carrier of n
m * ((Line (x,q2)) "*" (Col (i,i))) is Element of the carrier of n
mlt ((Line (x,q2)),(Col (i,i))) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (mlt ((Line (x,q2)),(Col (i,i)))) is Element of the carrier of n
m * (Sum (mlt ((Line (x,q2)),(Col (i,i))))) is Element of the carrier of n
m * (mlt ((Line (x,q2)),(Col (i,i)))) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (m * (mlt ((Line (x,q2)),(Col (i,i))))) is Element of the carrier of n
n is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of n
m * n is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of n
mlt ((Line (x,q2)),(m * n)) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() V39( width x) FinSequence-like FinSubsequence-like Element of (width x) -tuples_on the carrier of n
Sum (mlt ((Line (x,q2)),(m * n))) is Element of the carrier of n
mlt ((Line (x,q2)),(Col ((m * i),i))) is V13() V16( NAT ) V17( the carrier of n) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (mlt ((Line (x,q2)),(Col ((m * i),i)))) is Element of the carrier of n
len (m * i) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
REAL * is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
the carrier of F_Real * is V1() functional FinSequence-membered FinSequenceSet of the carrier of F_Real
n is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
n is set
n * is V1() functional FinSequence-membered FinSequenceSet of n
m is set
m * is V1() functional FinSequence-membered FinSequenceSet of m
x is V13() V16( NAT ) V17(n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of n *
Indices x is set
dom x is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width x) is V32() V39( width x) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom x),(Seg (width x))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
i is V13() V16( NAT ) V17(m * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of m *
j is ordinal natural ext-real non negative set
p is ordinal natural ext-real non negative set
[j,p] is set
x * (j,p) is Element of n
i * (j,p) is Element of m
x . j is FinSequence-like set
i . j is FinSequence-like set
q2 is V13() V16( NAT ) V17(m) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of m
q2 . p is set
i is V13() V16( NAT ) V17(n) Function-like V32() FinSequence-like FinSubsequence-like FinSequence of n
i . p is set
n is non empty non degenerated V49() right_complementable almost_left_invertible V98() V99() V100() unital V191() V193() right-distributive left-distributive right_unital well-unital V199() left_unital doubleLoopStr
the carrier of n is V1() V2() set
the carrier of n * is V1() functional FinSequence-membered FinSequenceSet of the carrier of n
m is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
m + x is V13() V16( NAT ) V17( the carrier of n * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
Indices (m + x) is set
dom (m + x) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (m + x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (m + x)) is V32() V39( width (m + x)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m + x)),(Seg (width (m + x)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices m is set
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
len (m + x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices n is set
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width n) is V32() V39( width n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom n),(Seg (width n))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
x is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[x,i] is set
(n,m) * (x,i) is V11() real ext-real Element of REAL
n * (x,i) is V11() real ext-real Element of REAL
m * (x,i) is V11() real ext-real Element of REAL
(n * (x,i)) + (m * (x,i)) is V11() real ext-real Element of REAL
(n) * (x,i) is V11() real ext-real Element of the carrier of F_Real
(m) * (x,i) is V11() real ext-real Element of the carrier of F_Real
((n) * (x,i)) + ((m) * (x,i)) is V11() real ext-real Element of the carrier of F_Real
K129(((n) * (x,i)),((m) * (x,i))) is V11() real ext-real Element of REAL
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices n is set
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width n) is V32() V39( width n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom n),(Seg (width n))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
Indices (n) is set
dom (n) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (n)) is V32() V39( width (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n)),(Seg (width (n)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
q2 is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[q2,i] is set
(x) * (q2,i) is V11() real ext-real Element of the carrier of F_Real
(n) * (q2,i) is V11() real ext-real Element of the carrier of F_Real
(m) * (q2,i) is V11() real ext-real Element of the carrier of F_Real
((n) * (q2,i)) + ((m) * (q2,i)) is V11() real ext-real Element of the carrier of F_Real
K129(((n) * (q2,i)),((m) * (q2,i))) is V11() real ext-real Element of REAL
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
- (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((- (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) - (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) - (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is real set
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
x is V11() real ext-real Element of the carrier of F_Real
x * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
j is V11() real ext-real Element of the carrier of F_Real
j * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((j * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
i is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
j is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
x is V11() real ext-real Element of the carrier of F_Real
x * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
x is V11() real ext-real Element of the carrier of F_Real
x * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len ((x * (m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width ((x * (m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Indices (n,m) is set
dom (n,m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (n,m)) is V32() V39( width (n,m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n,m)),(Seg (width (n,m)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices m is set
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Indices m is set
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
x is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[x,i] is set
(n,m) * (x,i) is V11() real ext-real Element of REAL
m * (x,i) is V11() real ext-real Element of REAL
n * (m * (x,i)) is V11() real ext-real Element of REAL
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
j is V11() real ext-real Element of the carrier of F_Real
j * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((j * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((j * (m))) * (x,i) is V11() real ext-real Element of REAL
(m) * (x,i) is V11() real ext-real Element of the carrier of F_Real
j * ((m) * (x,i)) is V11() real ext-real Element of the carrier of F_Real
K131(j,((m) * (x,i))) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
m @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (m @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices (n,(m @)) is set
dom (n,(m @)) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (n,(m @)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (n,(m @))) is V32() V39( width (n,(m @))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n,(m @))),(Seg (width (n,(m @))))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices (n,m) is set
dom (n,m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (n,m)) is V32() V39( width (n,m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n,m)),(Seg (width (n,m)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
x is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[x,i] is set
[i,x] is set
Indices (m @) is set
dom (m @) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (m @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (m @)) is V32() V39( width (m @)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m @)),(Seg (width (m @)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices m is set
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
x is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[i,x] is set
(n,(m @)) * (x,i) is V11() real ext-real Element of REAL
(n,m) * (i,x) is V11() real ext-real Element of REAL
Indices m is set
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
[x,i] is set
Indices (m @) is set
dom (m @) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (m @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (m @)) is V32() V39( width (m @)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m @)),(Seg (width (m @)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
(m @) * (x,i) is V11() real ext-real Element of REAL
n * ((m @) * (x,i)) is V11() real ext-real Element of REAL
m * (i,x) is V11() real ext-real Element of REAL
n * (m * (i,x)) is V11() real ext-real Element of REAL
len (n,(m @)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V11() real ext-real Element of REAL
m is ordinal natural ext-real non negative set
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom x is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
x . m is FinSequence-like set
(n,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,x) . m is FinSequence-like set
rng x is functional FinSequence-membered Element of K6((REAL *))
K6((REAL *)) is set
i is ordinal natural ext-real non negative set
len (n,x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
rng (n,x) is functional FinSequence-membered Element of K6((REAL *))
width (n,x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
j is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
p is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len p is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
q2 is ordinal natural ext-real non negative set
dom (n,x) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is ordinal natural ext-real non negative set
q is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len q is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
q is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n * q is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len (n * q) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
j is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
j is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
j is ordinal natural ext-real non negative set
i . j is set
(n * q) . j is V11() real ext-real Element of REAL
Seg (width x) is V32() V39( width x) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
[m,j] is set
Indices x is set
K7((dom x),(Seg (width x))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
[m,j] is set
Indices (n,x) is set
Seg (width (n,x)) is V32() V39( width (n,x)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n,x)),(Seg (width (n,x)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
(n,x) * (m,j) is V11() real ext-real Element of REAL
x * (m,j) is V11() real ext-real Element of REAL
i . j is set
q . j is V11() real ext-real Element of REAL
n * (q . j) is V11() real ext-real Element of REAL
c₁₃ is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
c₁₃ . j is V11() real ext-real Element of REAL
c₁₄ is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
c₁₄ . j is V11() real ext-real Element of REAL
j is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
j is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
j is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(1,n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
1_ F_Real is V11() real ext-real Element of the carrier of F_Real
K198(F_Real) is V11() real V51( F_Real ) ext-real Element of the carrier of F_Real
the OneF of F_Real is V11() real ext-real Element of the carrier of F_Real
(1_ F_Real) * (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((1_ F_Real) * (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
1_ F_Real is V11() real ext-real Element of the carrier of F_Real
K198(F_Real) is V11() real V51( F_Real ) ext-real Element of the carrier of F_Real
the OneF of F_Real is V11() real ext-real Element of the carrier of F_Real
(1_ F_Real) + (1_ F_Real) is V11() real ext-real Element of the carrier of F_Real
K129((1_ F_Real),(1_ F_Real)) is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(2,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(1_ F_Real) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((1_ F_Real) + (1_ F_Real)) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((1_ F_Real) + (1_ F_Real)) * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
1_ F_Real is V11() real ext-real Element of the carrier of F_Real
K198(F_Real) is V11() real V51( F_Real ) ext-real Element of the carrier of F_Real
the OneF of F_Real is V11() real ext-real Element of the carrier of F_Real
(1_ F_Real) + (1_ F_Real) is V11() real ext-real Element of the carrier of F_Real
K129((1_ F_Real),(1_ F_Real)) is V11() real ext-real Element of REAL
((1_ F_Real) + (1_ F_Real)) + (1_ F_Real) is V11() real ext-real Element of the carrier of F_Real
K129(((1_ F_Real) + (1_ F_Real)),(1_ F_Real)) is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,m),m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m,m)) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m,m)) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(3,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V11() real ext-real Element of the carrier of F_Real
n * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(1_ F_Real) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((1_ F_Real) + (1_ F_Real)) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((1_ F_Real) * (m)) + (((1_ F_Real) + (1_ F_Real)) * (m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((1_ F_Real) * (m)) + (((1_ F_Real) + (1_ F_Real)) * (m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) + (((1_ F_Real) + (1_ F_Real)) * (m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + (((1_ F_Real) + (1_ F_Real)) * (m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((1_ F_Real) * (m)) + ((1_ F_Real) * (m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) + (((1_ F_Real) * (m)) + ((1_ F_Real) * (m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + (((1_ F_Real) * (m)) + ((1_ F_Real) * (m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) + ((1_ F_Real) * (m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) + ((m) + ((1_ F_Real) * (m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + ((m) + ((1_ F_Real) * (m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) + ((m) + (m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + ((m) + (m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m) + (m)) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m) + (m)) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is ordinal natural ext-real non negative set
m is ordinal natural ext-real non negative set
0. (F_Real,n,m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
((0. (F_Real,n,m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
- (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((- (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) - ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) - ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
- ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((- ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (((m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (((m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is ordinal natural ext-real non negative set
m is ordinal natural ext-real non negative set
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,n,m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
((0. (F_Real,n,m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(x,(n,m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) + ((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) + ((n,m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m)) + (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n,m)) + (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (0. (F_Real,n,m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (0. (F_Real,n,m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
i + (0. (F_Real,n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((i + (0. (F_Real,n,m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((len n),(width n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,(len n),(width n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of len n, width n, the carrier of F_Real
((0. (F_Real,(len n),(width n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
- (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((- (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m),(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,m)) + ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n,m)) + ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) + (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m) + (n)) + (- (n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m) + (n)) + (- (n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m) + (n)) - (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m) + (n)) - (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((len n),(width n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,(len n),(width n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of len n, width n, the carrier of F_Real
((0. (F_Real,(len n),(width n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
- (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((- (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
- (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
len (- (m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (- (m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(((len n),(width n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
- (- (m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (- (- (m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) - (- (m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m,n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) - (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) - (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((len n),(width n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,(len n),(width n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of len n, width n, the carrier of F_Real
((0. (F_Real,(len n),(width n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) + (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,(n,x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) * ((n,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) * ((n,x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m,x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
i is V11() real ext-real Element of the carrier of F_Real
i * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((i * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((i * (x)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) * (((i * (x)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) * (((i * (x)))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((((m) * (x)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
i * ((((m) * (x)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((i * ((((m) * (x)))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,m)) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n,m)) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m,x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
m @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (m @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width (x @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,(m @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @),(n,(m @))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,(m @))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x @)) * ((n,(m @))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x @)) * ((n,(m @))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @),(m @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x @)) * ((m @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x @)) * ((m @)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,((x @),(m @))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,x) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,((m,x) @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width (n,(m,x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m,x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n,(m,x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m,x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,(m,x)) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @),((n,m) @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n,m) @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x @)) * (((n,m) @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x @)) * (((n,m) @)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m),x) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len ((n,m),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width ((n,m),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n,(m,x)) @) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((len n),(width n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,(len n),(width n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of len n, width n, the carrier of F_Real
((0. (F_Real,(len n),(width n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,((len n),(width n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((len n),(width n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (((len n),(width n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (((len n),(width n))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(((len n),(width n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
- (((len n),(width n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((- (((len n),(width n))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(((len n),(width n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((((len n),(width n)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + ((((len n),(width n)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + ((((len n),(width n)))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) - (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) - (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
- ((n,n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((- ((n,n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,((n,n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n,n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (((n,n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (((n,n))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) - ((n) - (n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) - ((n) - (n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is real set
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) + (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m,x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m),(n,x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,m)) + ((n,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n,m)) + ((n,x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
i is V11() real ext-real Element of the carrier of F_Real
i * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((i * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((i * (m)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((i * (m)))) + ((n,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((i * (m)))) + ((n,x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
i * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((i * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((i * (x)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(i * (m)) + (((i * (x)))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((i * (m)) + (((i * (x)))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(i * (m)) + (i * (x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((i * (m)) + (i * (x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
i * ((m,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((i * ((m,x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(0,n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((len n),(width n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,(len n),(width n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of len n, width n, the carrier of F_Real
((0. (F_Real,(len n),(width n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
0. F_Real is V11() real V51( F_Real ) ext-real Element of the carrier of F_Real
the ZeroF of F_Real is V11() real ext-real Element of the carrier of F_Real
(0. F_Real) * (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((0. F_Real) * (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom x is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
rng x is set
i is set
j is set
x . j is set
p is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n . p is V11() real ext-real Element of REAL
<*(n . p)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len <*(n . p)*> is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
rng i is functional FinSequence-membered Element of K6((REAL *))
K6((REAL *)) is set
j is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom i is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
p is ordinal natural ext-real non negative set
i . p is FinSequence-like set
n . p is V11() real ext-real Element of REAL
<*(n . p)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len <*(n . p)*> is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (len n) is V32() V39( len n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg m is V32() V39(m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
j is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of len i,1, REAL
width j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is ordinal natural ext-real non negative set
m . i is FinSequence-like set
n . i is V11() real ext-real Element of REAL
<*(n . i)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
x . i is FinSequence-like set
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom x is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (m,1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len m) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len m) -tuples_on REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len m) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
rng m is functional FinSequence-membered Element of K6((REAL *))
K6((REAL *)) is set
x is ordinal natural ext-real non negative set
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
i is ordinal natural ext-real non negative set
n . i is V11() real ext-real Element of REAL
m * (i,1) is V11() real ext-real Element of REAL
j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m . j is FinSequence-like set
n . j is V11() real ext-real Element of REAL
<*(n . j)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
p is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
p . 1 is V11() real ext-real Element of REAL
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
[j,1] is set
Indices m is set
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
j is ordinal natural ext-real non negative set
m . j is FinSequence-like set
n . j is V11() real ext-real Element of REAL
<*(n . j)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
p is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len p is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
[j,1] is set
Indices m is set
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
m * (j,1) is V11() real ext-real Element of REAL
p is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
p . 1 is V11() real ext-real Element of REAL
q2 is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len q2 is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n + m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n),(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) + ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) + ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (n)) is V32() V39( width (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg 1 is V1() V32() V39(1) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (n) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices (m) is set
dom (m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width (m)) is V32() V39( width (m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m)),(Seg (width (m)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices (n) is set
K7((dom (n)),(Seg (width (n)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
len (n + m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (n + m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len ((n + m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width ((n + m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices ((n + m)) is set
dom ((n + m)) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width ((n + m))) is V32() V39( width ((n + m))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom ((n + m))),(Seg (width ((n + m))))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
x is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[x,i] is set
((n + m)) * (x,i) is V11() real ext-real Element of REAL
(n) * (x,i) is V11() real ext-real Element of REAL
(m) * (x,i) is V11() real ext-real Element of REAL
((n) * (x,i)) + ((m) * (x,i)) is V11() real ext-real Element of REAL
(n) . x is FinSequence-like set
j is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
j . i is V11() real ext-real Element of REAL
n . x is V11() real ext-real Element of REAL
<*(n . x)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n + m)) . x is FinSequence-like set
p is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
p . i is V11() real ext-real Element of REAL
(m) . x is FinSequence-like set
q2 is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
q2 . i is V11() real ext-real Element of REAL
m . x is V11() real ext-real Element of REAL
<*(m . x)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n + m) . x is V11() real ext-real Element of REAL
<*((n + m) . x)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n * m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n * m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (n,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n * m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (n * m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom (m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
x is ordinal natural ext-real non negative set
(n,(m)) . x is FinSequence-like set
(n * m) . x is V11() real ext-real Element of REAL
<*((n * m) . x)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
rng (n,(m)) is functional FinSequence-membered Element of K6((REAL *))
K6((REAL *)) is set
i is ordinal natural ext-real non negative set
(m) . x is FinSequence-like set
m . x is V11() real ext-real Element of REAL
<*(m . x)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
dom (n,(m)) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
j is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
width (n,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
p is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len p is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len <*((n * m) . x)*> is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
q2 is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len q2 is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is V13() V16( NAT ) Function-like V32() FinSequence-like FinSubsequence-like set
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
width ((m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width ((m))) is V32() V39( width ((m))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
[x,1] is set
Indices ((m)) is set
dom ((m)) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom ((m))),(Seg (width ((m))))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
(m) * (x,1) is V11() real ext-real Element of REAL
Indices (n,(m)) is set
Seg (width (n,(m))) is V32() V39( width (n,(m))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n,(m))),(Seg (width (n,(m))))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
(n,(m)) * (x,1) is V11() real ext-real Element of REAL
j . 1 is V11() real ext-real Element of REAL
q2 is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m) * (q2,1) is V11() real ext-real Element of REAL
n * ((m) * (q2,1)) is V11() real ext-real Element of REAL
m . q2 is V11() real ext-real Element of REAL
n * (m . q2) is V11() real ext-real Element of REAL
(n * m) . q2 is V11() real ext-real Element of REAL
<*((n * m) . q2)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
<*((n * m) . q2)*> . 1 is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
i . 1 is V11() real ext-real Element of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
i . 1 is V11() real ext-real Element of REAL
len <*((n * m) . q2)*> is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is ordinal natural ext-real non negative set
j . i is V11() real ext-real Element of REAL
<*((n * m) . q2)*> . i is V11() real ext-real Element of REAL
width (n,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
<*n*> is V1() V13() V16( NAT ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like set
rng <*n*> is set
{n} is V1() set
x is set
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len <*n*> is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom x is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg 1 is V1() V32() V39(1) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
rng x is functional FinSequence-membered Element of K6((REAL *))
K6((REAL *)) is set
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len i is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is ordinal natural ext-real non negative set
x * (1,i) is V11() real ext-real Element of REAL
n . i is V11() real ext-real Element of REAL
Seg (len n) is V32() V39( len n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
<*n*> . 1 is set
[1,i] is set
Indices x is set
Seg (width x) is V32() V39( width x) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom x),(Seg (width x))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg 1 is V1() V32() V39(1) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Indices m is set
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom m),(Seg (width m))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
i is ordinal natural ext-real non negative set
j is ordinal natural ext-real non negative set
[i,j] is set
m * (i,j) is V11() real ext-real Element of REAL
x * (i,j) is V11() real ext-real Element of REAL
Seg (len n) is V32() V39( len n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
n . j is V11() real ext-real Element of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (m,1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width m) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width m) -tuples_on REAL
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width m) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
x is ordinal natural ext-real non negative set
m * (1,x) is V11() real ext-real Element of REAL
n . x is V11() real ext-real Element of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width m) is V32() V39( width m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
x is ordinal natural ext-real non negative set
n . x is V11() real ext-real Element of REAL
m * (1,x) is V11() real ext-real Element of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
dom (n) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (len (n)) is V32() V39( len (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (n) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (len (n)) is V32() V39( len (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Indices (n) is set
Seg (width (n)) is V32() V39( width (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n)),(Seg (width (n)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices (n) is set
Seg (width (n)) is V32() V39( width (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n)),(Seg (width (n)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
m is ordinal natural ext-real non negative set
x is ordinal natural ext-real non negative set
[m,x] is set
[x,m] is set
m is ordinal natural ext-real non negative set
x is ordinal natural ext-real non negative set
[x,m] is set
(n) * (m,x) is V11() real ext-real Element of REAL
(n) * (x,m) is V11() real ext-real Element of REAL
[m,x] is set
(n) . m is FinSequence-like set
Seg 1 is V1() V32() V39(1) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (len n) is V32() V39( len n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
n . m is V11() real ext-real Element of REAL
<*(n . m)*> is V1() V13() V16( NAT ) V17( REAL ) Function-like V32() V39(1) FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
i is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
i . x is V11() real ext-real Element of REAL
m is ordinal natural ext-real non negative set
x is ordinal natural ext-real non negative set
[x,m] is set
(n) * (m,x) is V11() real ext-real Element of REAL
(n) * (x,m) is V11() real ext-real Element of REAL
[m,x] is set
m is ordinal natural ext-real non negative set
x is ordinal natural ext-real non negative set
[m,x] is set
[x,m] is set
j is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[j,i] is set
[i,j] is set
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n + m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n),(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) + ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) + ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (n + m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (n + m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices (m) is set
dom (m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width (m)) is V32() V39( width (m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m)),(Seg (width (m)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices (n) is set
dom (n) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width (n)) is V32() V39( width (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n)),(Seg (width (n)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Seg (len n) is V32() V39( len n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (len (n)) is V32() V39( len (n)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg 1 is V1() V32() V39(1) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
width ((n + m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((n + m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices ((n + m)) is set
dom ((n + m)) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width ((n + m))) is V32() V39( width ((n + m))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom ((n + m))),(Seg (width ((n + m))))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
x is ordinal natural ext-real non negative set
i is ordinal natural ext-real non negative set
[x,i] is set
((n + m)) * (x,i) is V11() real ext-real Element of REAL
(n) * (x,i) is V11() real ext-real Element of REAL
(m) * (x,i) is V11() real ext-real Element of REAL
((n) * (x,i)) + ((m) * (x,i)) is V11() real ext-real Element of REAL
(n) . x is FinSequence-like set
j is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
j . i is V11() real ext-real Element of REAL
((n + m)) . x is FinSequence-like set
p is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
p . i is V11() real ext-real Element of REAL
(m) . x is FinSequence-like set
q2 is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
q2 . i is V11() real ext-real Element of REAL
n . i is V11() real ext-real Element of REAL
m . i is V11() real ext-real Element of REAL
(n + m) . i is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
n * m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n * m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (n,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n * m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom (n * m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (len (m)) is V32() V39( len (m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom (m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (len (n,(m))) is V32() V39( len (n,(m))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom (n,(m)) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
(n,(m)) . 1 is FinSequence-like set
rng (n,(m)) is functional FinSequence-membered Element of K6((REAL *))
K6((REAL *)) is set
i is ordinal natural ext-real non negative set
(n,(m)) * (1,i) is V11() real ext-real Element of REAL
(n * m) . i is V11() real ext-real Element of REAL
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Indices (n,(m)) is set
width (n,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width (n,(m))) is V32() V39( width (n,(m))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (n,(m))),(Seg (width (n,(m))))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Indices (m) is set
Seg (width (m)) is V32() V39( width (m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
K7((dom (m)),(Seg (width (m)))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
Seg (len m) is V32() V39( len m) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
[1,i] is set
x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x . j is V11() real ext-real Element of REAL
(m) * (1,j) is V11() real ext-real Element of REAL
n * ((m) * (1,j)) is V11() real ext-real Element of REAL
m . j is V11() real ext-real Element of REAL
n * (m . j) is V11() real ext-real Element of REAL
(n * m) . j is V11() real ext-real Element of REAL
p is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
p . i is V11() real ext-real Element of REAL
width (n,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n,(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) * ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) * ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((n,(m)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (n,(m))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (n,(m))) -tuples_on REAL
len (n,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (n,(m))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m),n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) * (n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m)) * (n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((m),n),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((m),n)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((m),n)) -tuples_on REAL
width ((m),n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((m),n)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width (m @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((m @),n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m @),(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m @)) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m @)) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((m @),(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((m @),(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((m @),(n))) -tuples_on REAL
len ((m @),(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((m @),(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(m,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n),m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((n),m),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((n),m)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((n),m)) -tuples_on REAL
width ((n),m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((n),m)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width ((m @),(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width ((m @),(n))) is V32() V39( width ((m @),(n))) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((n),m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n),m) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n),m) @) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((((n),m) @) @),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((((n),m) @) @)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((((n),m) @) @)) -tuples_on REAL
width ((((n),m) @) @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((((n),m) @) @)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(n) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m @),((n) @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n) @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m @)) * (((n) @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m @)) * (((n) @)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m @),((n) @)) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((m @),((n) @)) @),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((m @),((n) @)) @)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((m @),((n) @)) @)) -tuples_on REAL
width (((m @),((n) @)) @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((m @),((n) @)) @)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
((m @),(n)) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((m @),(n)) @),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((m @),(n)) @)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((m @),(n)) @)) -tuples_on REAL
width (((m @),(n)) @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((m @),(n)) @)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len (m @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((m,(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (m,(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (m,(n))) -tuples_on REAL
len (m,(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (m,(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
((m @),n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n),(m @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) * ((m @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) * ((m @)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((n),(m @)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((n),(m @))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((n),(m @))) -tuples_on REAL
width ((n),(m @)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((n),(m @))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
width (m @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m @) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((m @) @),n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(((m @) @),(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((m @) @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m @) @)) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((m @) @)) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((((m @) @),(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (((m @) @),(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (((m @) @),(n))) -tuples_on REAL
len (((m @) @),(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (((m @) @),(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom m is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
x is ordinal natural ext-real non negative set
Col ((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (n,m)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (n,m)) -tuples_on REAL
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (n,m)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
Col (n,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len n) -tuples_on REAL
(len n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
Col (m,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len m) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len m) -tuples_on REAL
(len m) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(Col (n,x)) + (Col (m,x)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len (Col (n,x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (Col (m,x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((Col (n,x)) + (Col (m,x))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Seg (width n) is V32() V39( width n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (len (n,m)) is V32() V39( len (n,m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom (n,m) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
dom ((Col (n,x)) + (Col (m,x))) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
i is ordinal natural ext-real non negative set
((Col (n,x)) + (Col (m,x))) . i is V11() real ext-real Element of REAL
(n,m) * (i,x) is V11() real ext-real Element of REAL
[i,x] is set
Indices n is set
K7((dom n),(Seg (width n))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(Col (n,x)) . j is V11() real ext-real Element of REAL
n * (j,x) is V11() real ext-real Element of REAL
(Col (m,x)) . j is V11() real ext-real Element of REAL
m * (j,x) is V11() real ext-real Element of REAL
((Col (n,x)) . j) + ((Col (m,x)) . j) is V11() real ext-real Element of REAL
(n,m) * (j,x) is V11() real ext-real Element of REAL
n is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(n) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(n) + (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n) + (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
x is ordinal natural ext-real non negative set
Line ((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (n,m)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (n,m)) -tuples_on REAL
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (n,m)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
Line (n,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width n) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width n) -tuples_on REAL
(width n) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
Line (m,x) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width m) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width m) -tuples_on REAL
(width m) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(Line (n,x)) + (Line (m,x)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len (Line (n,x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom n is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
len (Line (m,x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((Line (n,x)) + (Line (m,x))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
dom ((Line (n,x)) + (Line (m,x))) is V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width n) is V32() V39( width n) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
Seg (width (n,m)) is V32() V39( width (n,m)) V145() V146() V147() V148() V149() V150() Element of K6(NAT)
i is ordinal natural ext-real non negative set
((Line (n,x)) + (Line (m,x))) . i is V11() real ext-real Element of REAL
(n,m) * (x,i) is V11() real ext-real Element of REAL
[x,i] is set
Indices n is set
K7((dom n),(Seg (width n))) is V17( INT ) V17( RAT ) complex-yielding V109() V110() V111() set
(Line (n,x)) . i is V11() real ext-real Element of REAL
n * (x,i) is V11() real ext-real Element of REAL
j is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(Line (m,x)) . j is V11() real ext-real Element of REAL
m * (x,j) is V11() real ext-real Element of REAL
(Line (n,x)) . j is V11() real ext-real Element of REAL
((Line (n,x)) . j) + ((Line (m,x)) . j) is V11() real ext-real Element of REAL
(n,m) * (x,j) is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
i is ordinal natural ext-real non negative set
Col ((n,m),i) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (n,m)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (n,m)) -tuples_on REAL
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (n,m)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
Col (m,i) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len m) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len m) -tuples_on REAL
(len m) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n * (Col (m,i)) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len m) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len m) -tuples_on REAL
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
x is V11() real ext-real Element of the carrier of F_Real
x * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((x * (m))),i) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((x * (m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((x * (m)))) -tuples_on REAL
len ((x * (m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((x * (m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
Col ((m),i) is V13() V16( NAT ) V17( the carrier of F_Real) Function-like V32() V39( len (m)) FinSequence-like FinSubsequence-like Element of (len (m)) -tuples_on the carrier of F_Real
(len (m)) -tuples_on the carrier of F_Real is V1() functional FinSequence-membered FinSequenceSet of the carrier of F_Real
x * (Col ((m),i)) is V13() V16( NAT ) V17( the carrier of F_Real) Function-like V32() V39( len (m)) FinSequence-like FinSubsequence-like Element of (len (m)) -tuples_on the carrier of F_Real
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(x,(n + m)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n + m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x,((n + m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n + m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) * (((n + m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * (((n + m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,((n + m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,((n + m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,((n + m)))) -tuples_on REAL
len (x,((n + m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,((n + m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x,(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,(n))) -tuples_on REAL
len (x,(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x,(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) * ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,(m)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,(m))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,(m))) -tuples_on REAL
len (x,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,(m))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,n) + (x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (x,(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n),(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) + ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) + ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x,((n),(m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n),(m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) * (((n),(m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * (((n),(m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,((n),(m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,((n),(m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,((n),(m)))) -tuples_on REAL
len (x,((n),(m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,((n),(m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
((x,(n)),(x,(m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x,(n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x,(m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x,(n))) + ((x,(m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x,(n))) + ((x,(m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((x,(n)),(x,(m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((x,(n)),(x,(m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((x,(n)),(x,(m)))) -tuples_on REAL
len ((x,(n)),(x,(m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((x,(n)),(x,(m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n + m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(x,(n + m)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n + m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n + m)),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n + m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n + m))) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((n + m))) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((n + m)),x),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((n + m)),x)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((n + m)),x)) -tuples_on REAL
width (((n + m)),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((n + m)),x)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((n),x),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((n),x)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((n),x)) -tuples_on REAL
width ((n),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((n),x)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m)) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((m),x),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((m),x)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((m),x)) -tuples_on REAL
width ((m),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((m),x)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,n) + (x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((n),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n),(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) + ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) + ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n),(m)),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n),(m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n),(m))) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((n),(m))) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((n),(m)),x),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((n),(m)),x)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((n),(m)),x)) -tuples_on REAL
width (((n),(m)),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((n),(m)),x)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(((n),x),((m),x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n),x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m),x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n),x)) + (((m),x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((n),x)) + (((m),x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((n),x),((m),x)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((n),x),((m),x))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((n),x),((m),x))) -tuples_on REAL
width (((n),x),((m),x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((n),x),((m),x))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n * m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(x,(n * m)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n * m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x,((n * m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n * m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) * (((n * m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * (((n * m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,((n * m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,((n * m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,((n * m)))) -tuples_on REAL
len (x,((n * m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,((n * m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x,(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) * ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,(m)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,(m))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,(m))) -tuples_on REAL
len (x,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,(m))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n * (x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (x,(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x,(n,(m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,(m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) * ((n,(m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * ((n,(m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,(n,(m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,(n,(m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,(n,(m)))) -tuples_on REAL
len (x,(n,(m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,(n,(m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(n,(x,(m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((n,(x,(m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (n,(x,(m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (n,(x,(m)))) -tuples_on REAL
len (n,(x,(m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (n,(x,(m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V11() real ext-real Element of REAL
m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n * m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(x,(n * m)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n * m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n * m)),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n * m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n * m))) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((n * m))) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((n * m)),x),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((n * m)),x)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((n * m)),x)) -tuples_on REAL
width (((n * m)),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((n * m)),x)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m)) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((m),x),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((m),x)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((m),x)) -tuples_on REAL
width ((m),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((m),x)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n * (x,m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
x @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @),m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @),(m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x @)) * ((m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x @)) * ((m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((x @),(m)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((x @),(m))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((x @),(m))) -tuples_on REAL
len ((x @),(m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((x @),(m))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
width (x @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((x @),(n * m)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n * m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x @),((n * m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n * m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x @)) * (((n * m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x @)) * (((n * m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((x @),((n * m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((x @),((n * m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((x @),((n * m)))) -tuples_on REAL
len ((x @),((n * m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((x @),((n * m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n * ((x @),m) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len (n * m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (x @) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(x @) @ is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((x @) @),(n * m)) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(((n * m)),((x @) @)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((x @) @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n * m))) * (((x @) @)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((n * m))) * (((x @) @)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((n * m)),((x @) @)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((n * m)),((x @) @))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((n * m)),((x @) @))) -tuples_on REAL
width (((n * m)),((x @) @)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((n * m)),((x @) @))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m,(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((m,(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (m,(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (m,(n))) -tuples_on REAL
len (m,(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (m,(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
len (m,n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (Col ((m,(n)),1)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n),m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((n),m),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((n),m)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((n),m)) -tuples_on REAL
width ((n),m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((n),m)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
len (m,n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (Line (((n),m),1)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width ((((n)) * (m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) + (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,x),n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,x),(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m,x)) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m,x)) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((m,x),(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((m,x),(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((m,x),(n))) -tuples_on REAL
len ((m,x),(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((m,x),(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(m,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(m,(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((m,(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (m,(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (m,(n))) -tuples_on REAL
len (m,(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (m,(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(x,(n)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(x) * ((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((x) * ((n)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((x,(n)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (x,(n))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (x,(n))) -tuples_on REAL
len (x,(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (x,(n))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(m,n) + (x,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (m,(n)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((m,(n)),(x,(n))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,(n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x,(n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m,(n))) + ((x,(n))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((m,(n))) + ((x,(n))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((m,(n)),(x,(n))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((m,(n)),(x,(n)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((m,(n)),(x,(n)))) -tuples_on REAL
len ((m,(n)),(x,(n))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((m,(n)),(x,(n)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
x is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(m,x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(m) + (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((m) + (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((m,x),n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(n) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n),(m,x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((m,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n)) * ((m,x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) * ((m,x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((n),(m,x)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((n),(m,x))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((n),(m,x))) -tuples_on REAL
width ((n),(m,x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((n),(m,x))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(m,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n),m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) * (m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) * (m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((n),m),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((n),m)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((n),m)) -tuples_on REAL
width ((n),m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((n),m)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(x,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((n),x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n)) * (x) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n)) * (x))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((n),x),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((n),x)) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((n),x)) -tuples_on REAL
width ((n),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((n),x)) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
(m,n) + (x,n) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
width (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((n),m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(((n),m),((n),x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n),m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n),x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n),m)) + (((n),x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((n),m)) + (((n),x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line ((((n),m),((n),x)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width (((n),m),((n),x))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width (((n),m),((n),x))) -tuples_on REAL
width (((n),m),((n),x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width (((n),m),((n),x))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,n,m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
((0. (F_Real,n,m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0* n is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of REAL n
REAL n is functional FinSequence-membered FinSequenceSet of REAL
x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m),(x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,m)) * ((x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n,m)) * ((x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col (((n,m),(x)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len ((n,m),(x))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len ((n,m),(x))) -tuples_on REAL
len ((n,m),(x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len ((n,m),(x))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((n,m),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n,m),(n,m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m)) + ((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n,m)) + ((n,m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n,m),(n,m)),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(((n,m),(n,m)),(x)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n,m),(n,m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((n,m),(n,m))) * ((x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
(((((n,m),(n,m))) * ((x)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Col ((((n,m),(n,m)),(x)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( len (((n,m),(n,m)),(x))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (len (((n,m),(n,m)),(x))) -tuples_on REAL
len (((n,m),(n,m)),(x)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(len (((n,m),(n,m)),(x))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
((n,m),x) + ((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(((n,m),x) + ((n,m),x)) - ((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(((n,m),x)) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * ((n,m),x) is V13() Function-like set
K306((((n,m),x) + ((n,m),x)),K335(((n,m),x))) is V13() Function-like set
n is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
m is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(n,m) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0. (F_Real,n,m) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
((0. (F_Real,n,m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
0* m is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of REAL m
REAL m is functional FinSequence-membered FinSequenceSet of REAL
x is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
len x is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(x) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x),(n,m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((x)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x)) * ((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x)) * ((n,m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((x),(n,m)),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((x),(n,m))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((x),(n,m))) -tuples_on REAL
width ((x),(n,m)) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((x),(n,m))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
len (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
len ((n,m),x) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
width (n,m) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
((n,m),(n,m)) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
((n,m)) + ((n,m)) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((n,m)) + ((n,m)))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n,m),(n,m)),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
((x),((n,m),(n,m))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
(((n,m),(n,m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((x)) * (((n,m),(n,m))) is V13() V16( NAT ) V17( the carrier of F_Real * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of F_Real *
((((x)) * (((n,m),(n,m))))) is V13() V16( NAT ) V17(REAL * ) Function-like V32() FinSequence-like FinSubsequence-like tabular FinSequence of REAL *
Line (((x),((n,m),(n,m))),1) is V13() V16( NAT ) V17( REAL ) Function-like V32() V39( width ((x),((n,m),(n,m)))) FinSequence-like FinSubsequence-like complex-yielding V109() V110() Element of (width ((x),((n,m),(n,m)))) -tuples_on REAL
width ((x),((n,m),(n,m))) is ordinal natural V11() real V30() V31() ext-real non negative V145() V146() V147() V148() V149() V150() Element of NAT
(width ((x),((n,m),(n,m)))) -tuples_on REAL is V1() functional FinSequence-membered FinSequenceSet of REAL
((n,m),x) + ((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
(((n,m),x) + ((n,m),x)) - ((n,m),x) is V13() V16( NAT ) V17( REAL ) Function-like V32() FinSequence-like FinSubsequence-like complex-yielding V109() V110() FinSequence of REAL
K335(((n,m),x)) is V13() Function-like complex-yielding set
K38(1) is V11() set
K38(1) * ((n,m),x) is V13() Function-like set
K306((((n,m),x) + ((n,m),x)),K335(((n,m),x))) is V13() Function-like set