:: MATRTOP2 semantic presentation

REAL is non empty V12() non finite V183() V184() V185() V189() set
NAT is non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() Element of K19(REAL)
K19(REAL) is non empty V12() non finite set
INT is non empty V12() non finite V183() V184() V185() V186() V187() V189() set

the carrier of K876() is set
COMPLEX is non empty V12() non finite V183() V189() set
RAT is non empty V12() non finite V183() V184() V185() V186() V189() set
K20(COMPLEX,COMPLEX) is Relation-like non empty V12() non finite complex-valued set
K19(K20(COMPLEX,COMPLEX)) is non empty V12() non finite set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is Relation-like non empty V12() non finite complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is non empty V12() non finite set

K19(K20(REAL,REAL)) is non empty V12() non finite set

K19(K20(K20(REAL,REAL),REAL)) is non empty V12() non finite set

K19(K20(RAT,RAT)) is non empty V12() non finite set

K19(K20(K20(RAT,RAT),RAT)) is non empty V12() non finite set

K19(K20(INT,INT)) is non empty V12() non finite set

K19(K20(K20(INT,INT),INT)) is non empty V12() non finite set

K19(K20(K20(NAT,NAT),NAT)) is non empty V12() non finite set
NAT is non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() set
K19(NAT) is non empty V12() non finite set
K19(NAT) is non empty V12() non finite set
K238() is set
1 is non empty V23() V27() V28() V29() V30() V31() finite cardinal ext-real positive non negative V183() V184() V185() V186() V187() V188() Element of NAT

2 is non empty V23() V27() V28() V29() V30() V31() finite cardinal ext-real positive non negative V183() V184() V185() V186() V187() V188() Element of NAT
{} is set

0 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
K624(0,1,2) is finite V183() V184() V185() V186() V187() V188() set

K19(K20(K20(K624(0,1,2),K624(0,1,2)),K624(0,1,2))) is finite V38() set
K19(K20(K624(0,1,2),K624(0,1,2))) is finite V38() set

K19(K20(1,1)) is finite V38() set

K19(K20(K20(1,1),1)) is finite V38() set

K19(K20(K20(1,1),REAL)) is set

K19(K20(K20(2,2),REAL)) is set

the carrier of () is non empty set

doubleLoopStr(# REAL,K143(),K145(),1,0 #) is strict doubleLoopStr
the carrier of F_Real is non empty V12() V183() V184() V185() set
K741() is non empty strict multMagma
the carrier of K741() is non empty set
K746() is non empty strict V139() V140() V141() V143() V247() V248() V249() V250() V251() V252() multMagma
K747() is non empty strict V141() V143() V250() V251() V252() M32(K746())
K748() is non empty strict V139() V141() V143() V250() V251() V252() V253() M35(K746(),K747())
K750() is non empty strict V139() V141() V143() multMagma
K751() is non empty strict V139() V141() V143() V253() M32(K750())

K19(K20(NAT,REAL)) is non empty V12() non finite set
3 is non empty V23() V27() V28() V29() V30() V31() finite cardinal ext-real positive non negative V183() V184() V185() V186() V187() V188() Element of NAT
Seg 1 is non empty V12() finite 1 -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
the carrier of F_Real * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
0. F_Real is V28() V29() V64( F_Real ) ext-real Element of the carrier of F_Real
the ZeroF of F_Real is V28() V29() ext-real Element of the carrier of F_Real

Sum () is V28() V29() ext-real Element of REAL
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set

the carrier of () is non empty set

m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set
the ZeroF of () is Relation-like Function-like Element of the carrier of ()

the carrier of () is non empty set

m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set

len n is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT

m is set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set

the carrier of () is non empty set
K19( the carrier of ()) is set

TRm is finite Element of K19( the carrier of ())

TRn . A is set
Funcs ( the carrier of (),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (), REAL
K19( the carrier of ()) is set

TRm is finite Element of K19( the carrier of ())
A is Relation-like Function-like Element of the carrier of ()
TRn . A is V28() V29() ext-real set
Funcs ( the carrier of (), the carrier of F_Real) is functional non empty FUNCTION_DOMAIN of the carrier of (), the carrier of F_Real
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set

the carrier of () is non empty set

Carrier MT is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set

Carrier TRn is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set
TRm is set

R is Relation-like Function-like Element of the carrier of ()
MT . R is V28() V29() ext-real Element of the carrier of F_Real
TRm is set
A is Relation-like Function-like Element of the carrier of ()
MT . A is V28() V29() ext-real Element of the carrier of F_Real

m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set
K20( the carrier of (),REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (),REAL)) is non empty V12() non finite set

the carrier of () is non empty set

K19(K20( the carrier of (), the carrier of F_Real)) is set

len (TRn (#) MT) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
len MT is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
len (M (#) n) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
len n is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
A is V23() V27() V28() V29() finite cardinal ext-real non negative set

MT /. A is Relation-like Function-like Element of the carrier of ()

the carrier of TRm is non empty set
dom (TRn (#) MT) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom n is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
n . A is set
dom MT is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
MT . A is set
dom (M (#) n) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(M (#) n) . A is set
x is Element of the carrier of TRm
M . x is V28() V29() ext-real set
(M . x) * x is Element of the carrier of TRm

M . R is V28() V29() ext-real set

TRn . (MT /. A) is V28() V29() ext-real Element of the carrier of F_Real

(TRn . (MT /. A)) * (MT /. A) is Relation-like Function-like Element of the carrier of ()
the lmult of () is Relation-like K20( the carrier of F_Real, the carrier of ()) -defined the carrier of () -valued Function-like total quasi_total Element of K19(K20(K20( the carrier of F_Real, the carrier of ()), the carrier of ()))
K20( the carrier of F_Real, the carrier of ()) is Relation-like set
K20(K20( the carrier of F_Real, the carrier of ()), the carrier of ()) is Relation-like set
K19(K20(K20( the carrier of F_Real, the carrier of ()), the carrier of ())) is set
K329( the carrier of F_Real, the carrier of (), the carrier of (), the lmult of (),(TRn . (MT /. A)),(MT /. A)) is Relation-like Function-like Element of the carrier of ()
(TRn (#) MT) . A is set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set

the carrier of () is non empty set

Sum TRn is Relation-like Function-like Element of the carrier of ()

the carrier of TRm is non empty set
K20(NAT, the carrier of TRm) is Relation-like non empty V12() non finite set
K19(K20(NAT, the carrier of TRm)) is non empty V12() non finite set
len MT is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
0. TRm is V64(TRm) Element of the carrier of TRm
the ZeroF of TRm is Element of the carrier of TRm
A is Relation-like NAT -defined the carrier of TRm -valued Function-like non empty total quasi_total Element of K19(K20(NAT, the carrier of TRm))
A . (len MT) is Element of the carrier of TRm
A . 0 is Element of the carrier of TRm
K20(NAT, the carrier of ()) is Relation-like non empty V12() non finite set
K19(K20(NAT, the carrier of ())) is non empty V12() non finite set
len TRn is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT

the ZeroF of () is Relation-like Function-like Element of the carrier of ()
R is Relation-like NAT -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20(NAT, the carrier of ()))
R . (len TRn) is Relation-like Function-like Element of the carrier of ()
R . 0 is Relation-like Function-like Element of the carrier of ()
v is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
A . v is set
R . v is set
v + 1 is non empty V23() V27() V28() V29() V30() V31() finite cardinal ext-real positive non negative V183() V184() V185() V186() V187() V188() Element of NAT
A . (v + 1) is set
R . (v + 1) is set

TRn /. (v + 1) is Relation-like Function-like Element of the carrier of ()
R . v is Relation-like Function-like Element of the carrier of ()

dom MT is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
MT . (v + 1) is set
A . (v + 1) is Element of the carrier of TRm
A . v is Element of the carrier of TRm
L is Element of the carrier of TRm
(A . v) + L is Element of the carrier of TRm
TRn . (v + 1) is set

(R . v) + (TRn /. (v + 1)) is Relation-like Function-like Element of the carrier of ()
R . (v + 1) is Relation-like Function-like Element of the carrier of ()
A . 0 is set
R . 0 is set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set

the carrier of () is non empty set

Sum MT is Relation-like Function-like Element of the carrier of ()

Carrier TRn is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set

rng TRm is finite Element of K19( the carrier of ())

Carrier MT is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set
Sum (MT (#) A) is Relation-like Function-like Element of the carrier of ()
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set
K19( the carrier of ()) is set

the carrier of () is non empty set
K19( the carrier of ()) is set
MT is Element of K19( the carrier of ())

[#] (Lin MT) is non empty non proper Element of K19( the carrier of (Lin MT))
the carrier of (Lin MT) is non empty set
K19( the carrier of (Lin MT)) is set
TRn is Element of K19( the carrier of ())

[#] (Lin TRn) is non empty non proper Element of K19( the carrier of (Lin TRn))
the carrier of (Lin TRn) is non empty set
K19( the carrier of (Lin TRn)) is set
TRm is set

Carrier R is finite Element of K19( the carrier of ())
Carrier A is finite Element of K19( the carrier of ())
Sum R is Relation-like Function-like Element of the carrier of ()
TRm is set

Sum A is Relation-like Function-like Element of the carrier of ()

Carrier R is finite Element of K19( the carrier of ())
Carrier A is finite Element of K19( the carrier of ())

m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set
K19( the carrier of ()) is set

the carrier of () is non empty set
K19( the carrier of ()) is set
M is Element of K19( the carrier of ())
TRn is Element of K19( the carrier of ())

Carrier A is finite Element of K19( the carrier of ())
Carrier TRm is finite Element of K19( the carrier of ())

the ZeroF of () is Relation-like Function-like Element of the carrier of ()
Sum A is Relation-like Function-like Element of the carrier of ()

Carrier A is finite Element of K19( the carrier of ())
Carrier TRm is finite Element of K19( the carrier of ())
Sum TRm is Relation-like Function-like Element of the carrier of ()

the carrier of m is non empty V12() set

the carrier of n is non empty set

the carrier of M is non empty set

MT | the carrier of M is Relation-like the carrier of n -defined the carrier of M -defined the carrier of n -defined the carrier of m -valued Function-like Element of K19(K20( the carrier of n, the carrier of m))
K20( the carrier of n, the carrier of m) is Relation-like set
K19(K20( the carrier of n, the carrier of m)) is set
[#] n is non empty non proper Element of K19( the carrier of n)
K19( the carrier of n) is set
K20( the carrier of M, the carrier of m) is Relation-like set
K19(K20( the carrier of M, the carrier of m)) is set
Funcs ( the carrier of M, the carrier of m) is functional non empty FUNCTION_DOMAIN of the carrier of M, the carrier of m
Carrier MT is finite Element of K19( the carrier of n)
(Carrier MT) /\ the carrier of M is finite Element of K19( the carrier of n)
TRm is Relation-like the carrier of M -defined the carrier of m -valued Function-like total quasi_total Element of Funcs ( the carrier of M, the carrier of m)
0. m is V64(m) Element of the carrier of m
the ZeroF of m is Element of the carrier of m
A is Element of the carrier of M
TRm . A is Element of the carrier of m
R is Element of the carrier of n
MT . R is Element of the carrier of m

the carrier of m is non empty V12() set

the carrier of n is non empty set
K19( the carrier of n) is set
M is linearly-independent Element of K19( the carrier of n)

Carrier MT is finite Element of K19( the carrier of n)

Carrier TRn is finite Element of K19( the carrier of n)
Sum MT is Element of the carrier of n
Sum TRn is Element of the carrier of n

Sum (MT - TRn) is Element of the carrier of n
(Sum MT) - (Sum TRn) is Element of the carrier of n
0. n is V64(n) Element of the carrier of n
the ZeroF of n is Element of the carrier of n
Carrier (MT - TRn) is finite Element of K19( the carrier of n)

MT + (- TRn) is Relation-like the carrier of n -defined the carrier of m -valued Function-like total quasi_total Linear_Combination of n
(- TRn) + MT is Relation-like the carrier of n -defined the carrier of m -valued Function-like total quasi_total Linear_Combination of n
- (- TRn) is Relation-like the carrier of n -defined the carrier of m -valued Function-like total quasi_total Linear_Combination of n

the carrier of m is non empty set

the carrier of n is non empty set

M | the carrier of n is Relation-like the carrier of m -defined the carrier of n -defined the carrier of m -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of m,REAL))
K20( the carrier of m,REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of m,REAL)) is non empty V12() non finite set
[#] m is non empty non proper Element of K19( the carrier of m)
K19( the carrier of m) is set
K20( the carrier of n,REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of n,REAL)) is non empty V12() non finite set
Funcs ( the carrier of n,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of n, REAL
Carrier M is finite Element of K19( the carrier of m)
() /\ the carrier of n is finite Element of K19( the carrier of m)

TRm is Element of the carrier of n
TRn . TRm is V28() V29() ext-real Element of REAL
A is Element of the carrier of m
M . A is V28() V29() ext-real Element of REAL
m is set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set

[#] TRn is non empty non proper Element of K19( the carrier of TRn)
the carrier of TRn is non empty set
K19( the carrier of TRn) is set

[#] TRm is non empty non proper Element of K19( the carrier of TRm)
the carrier of TRm is non empty set
K19( the carrier of TRm) is set

R is finite Element of K19( the carrier of TRn)

R is finite Element of K19( the carrier of TRm)
v is Element of the carrier of TRn
A . v is V28() V29() ext-real set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of MT is non empty set

the carrier of TRn is non empty set

Carrier TRm is finite Element of K19( the carrier of MT)
K19( the carrier of MT) is set
Sum TRm is Element of the carrier of MT

Carrier A is finite Element of K19( the carrier of TRn)
K19( the carrier of TRn) is set
Sum A is Element of the carrier of TRn
K20( the carrier of TRn,REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of TRn,REAL)) is non empty V12() non finite set
dom TRm is Element of K19( the carrier of MT)
[#] MT is non empty non proper Element of K19( the carrier of MT)
dom A is Element of K19( the carrier of TRn)
[#] TRn is non empty non proper Element of K19( the carrier of TRn)
the carrier of () is non empty set
v is set
A . v is V28() V29() ext-real set

x is Element of the carrier of TRn
A . x is V28() V29() ext-real Element of REAL
A . x is V28() V29() ext-real set

K20( the carrier of (),REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (),REAL)) is non empty V12() non finite set

K19( the carrier of ()) is set
Funcs ( the carrier of (),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (), REAL

x is finite Element of K19( the carrier of ())
A . x is V28() V29() ext-real set
v . x is V28() V29() ext-real Element of REAL

x | the carrier of TRn is Relation-like the carrier of TRn -defined the carrier of () -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (),REAL))
L is set
x . L is V28() V29() ext-real set
A . L is V28() V29() ext-real set

R . L is V28() V29() ext-real set

R . L is V28() V29() ext-real set
the carrier of () is non empty set
C is set
Carrier x is finite Element of K19( the carrier of ())

x . F is V28() V29() ext-real Element of REAL
A . F is V28() V29() ext-real set

Carrier L is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set
Sum L is Relation-like Function-like Element of the carrier of ()

m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set
K19( the carrier of ()) is set
M is Element of K19( the carrier of ())

m is V23() V27() V28() V29() finite cardinal ext-real non negative set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set

lines M is finite Element of K19( the carrier of ())
the carrier of () is non empty set
K19( the carrier of ()) is set

[#] (Lin ()) is non empty non proper Element of K19( the carrier of (Lin ()))
the carrier of (Lin ()) is non empty set
K19( the carrier of (Lin ())) is set
MT is set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

n is V23() V27() V28() V29() finite cardinal ext-real non negative set

the_rank_of M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
lines M is finite Element of K19( the carrier of ())
the carrier of () is non empty set
K19( the carrier of ()) is set

the carrier of (Lin ()) is non empty set
[#] (Lin ()) is non empty non proper Element of K19( the carrier of (Lin ()))
K19( the carrier of (Lin ())) is set
MT is Element of K19( the carrier of (Lin ()))

TRn is Relation-like NAT -defined the carrier of (Lin ()) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Lin ())

the carrier of m is non empty V12() set

the carrier of n is non empty set

the carrier of M is non empty set
K20( the carrier of n, the carrier of M) is Relation-like set
K19(K20( the carrier of n, the carrier of M)) is set
K19( the carrier of n) is set
MT is Relation-like the carrier of n -defined the carrier of M -valued Function-like non empty total quasi_total V157(n,M) V200(m,n,M) Element of K19(K20( the carrier of n, the carrier of M))
TRn is Element of K19( the carrier of n)
MT | TRn is Relation-like the carrier of n -defined TRn -defined the carrier of n -defined the carrier of M -valued Function-like Element of K19(K20( the carrier of n, the carrier of M))

Sum TRm is Element of the carrier of n
MT . (Sum TRm) is Element of the carrier of M

Sum (MT @ TRm) is Element of the carrier of M
Carrier TRm is finite Element of K19( the carrier of n)

rng A is finite Element of K19( the carrier of n)

Sum (TRm (#) A) is Element of the carrier of n

(MT | TRn) | (Carrier TRm) is Relation-like the carrier of n -defined Carrier TRm -defined the carrier of n -defined the carrier of M -valued Function-like finite Element of K19(K20( the carrier of n, the carrier of M))
MT | (Carrier TRm) is Relation-like the carrier of n -defined Carrier TRm -defined the carrier of n -defined the carrier of M -valued Function-like finite Element of K19(K20( the carrier of n, the carrier of M))

rng v is finite Element of K19( the carrier of M)
K19( the carrier of M) is set
MT .: (Carrier TRm) is finite Element of K19( the carrier of M)
Carrier (MT @ TRm) is finite Element of K19( the carrier of M)
dom MT is non empty Element of K19( the carrier of n)
[#] n is non empty non proper Element of K19( the carrier of n)

Sum ((MT @ TRm) (#) v) is Element of the carrier of M

m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
Seg n is finite n -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

Sum M is V28() V29() ext-real set
dom M is finite n -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)

lines MT is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set
card (lines MT) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Mx2Tran MT is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (), the carrier of ()))

the carrier of () is non empty set

the carrier of () is non empty set
K20( the carrier of (), the carrier of ()) is Relation-like set
K19(K20( the carrier of (), the carrier of ())) is set

len MT is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
len ((Mx2Tran MT) . M) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
len M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
R is set
{R} is non empty V12() finite 1 -element set
dom MT is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
v is set

width MT is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
x is V23() V27() V28() V29() finite cardinal ext-real non negative set

(width MT) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real

K19(K20( the carrier of (), the carrier of F_Real)) is set
x is Relation-like Function-like Element of the carrier of ()
1. F_Real is V28() V29() V64( F_Real ) ext-real Element of the carrier of F_Real
the OneF of F_Real is V28() V29() ext-real Element of the carrier of F_Real

R . x is V28() V29() ext-real Element of the carrier of F_Real
Funcs ( the carrier of (), the carrier of F_Real) is functional non empty FUNCTION_DOMAIN of the carrier of (), the carrier of F_Real
C is Relation-like Function-like Element of the carrier of ()
L is Relation-like the carrier of () -defined the carrier of F_Real -valued Function-like total quasi_total Element of Funcs ( the carrier of (), the carrier of F_Real)
L . C is V28() V29() ext-real Element of the carrier of F_Real
TRn is V28() V29() ext-real Element of the carrier of F_Real

len (TRn * (Line (MT,x))) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT

len (@ M) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT

F is V23() V27() V28() V29() finite cardinal ext-real non negative set
MT * (x,F) is V28() V29() ext-real Element of the carrier of F_Real
dom (TRn * (Line (MT,x))) is finite width MT -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Seg m is finite m -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(Line (MT,x)) . F is set
F is V23() V27() V28() V29() finite cardinal ext-real non negative set

(len MT) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
(Col (MT,F)) . F is set
MT * (F,F) is V28() V29() ext-real Element of the carrier of F_Real
(Line (MT,F)) . F is set

(n |-> (MT * (x,F))) . F is V28() V29() ext-real set
len (Col (MT,F)) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
len (n |-> (MT * (x,F))) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
((Mx2Tran MT) . M) . F is V28() V29() ext-real set
(@ M) "*" (Col (MT,F)) is V28() V29() ext-real Element of the carrier of F_Real

Sum (mlt ((@ M),(Col (MT,F)))) is V28() V29() ext-real Element of the carrier of F_Real

Sum ((MT * (x,F)) * C) is V28() V29() ext-real Element of the carrier of F_Real
Sum (@ M) is V28() V29() ext-real Element of the carrier of F_Real
(MT * (x,F)) * (Sum (@ M)) is V28() V29() ext-real Element of the carrier of F_Real
(MT * (x,F)) * (Sum (@ M)) is V28() V29() ext-real Element of REAL
(MT * (x,F)) * TRn is V28() V29() ext-real Element of the carrier of F_Real
(MT * (x,F)) * TRn is V28() V29() ext-real Element of REAL
(TRn * (Line (MT,x))) . F is set

Carrier C is finite Element of K19( the carrier of ())

F is set
C . F is set

Sum F is Relation-like Function-like Element of the carrier of ()
() * x is Relation-like Function-like Element of the carrier of ()
the lmult of () is Relation-like K20( the carrier of F_Real, the carrier of ()) -defined the carrier of () -valued Function-like total quasi_total Element of K19(K20(K20( the carrier of F_Real, the carrier of ()), the carrier of ()))
K20( the carrier of F_Real, the carrier of ()) is Relation-like set
K20(K20( the carrier of F_Real, the carrier of ()), the carrier of ()) is Relation-like set
K19(K20(K20( the carrier of F_Real, the carrier of ()), the carrier of ())) is set
K329( the carrier of F_Real, the carrier of (), the carrier of (), the lmult of (),(),x) is Relation-like Function-like Element of the carrier of ()

Sum F is Relation-like Function-like Element of the carrier of ()
TRn * (Sum F) is Relation-like Function-like Element of the carrier of ()
K329( the carrier of F_Real, the carrier of (), the carrier of (), the lmult of (),TRn,(Sum F)) is Relation-like Function-like Element of the carrier of ()
F is V23() V27() V28() V29() finite cardinal ext-real non negative set

F . (Line (MT,F)) is set
{(Line (MT,F))} is functional non empty V12() finite V38() 1 -element set
MT " {(Line (MT,F))} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
TRn * () is V28() V29() ext-real Element of the carrier of F_Real
TRn * () is V28() V29() ext-real Element of REAL

Sum TRn is Relation-like Function-like Element of the carrier of ()

the ZeroF of () is Relation-like Function-like Element of the carrier of ()

TRm is V23() V27() V28() V29() finite cardinal ext-real non negative set

width MT is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(width MT) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
TRn . (Line (MT,TRm)) is set
{(Line (MT,TRm))} is functional non empty V12() finite V38() 1 -element set
MT " {(Line (MT,TRm))} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
m is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
Seg n is finite n -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
K19((Seg n)) is finite V38() set

lines MT is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set
Mx2Tran MT is Relation-like the carrier of () -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (), the carrier of ()))

the carrier of () is non empty set

the carrier of () is non empty set
K20( the carrier of (), the carrier of ()) is Relation-like set
K19(K20( the carrier of (), the carrier of ())) is set

TRn is V23() V27() V28() V29() finite cardinal ext-real non negative set
TRn + 1 is non empty V23() V27() V28() V29() V30() V31() finite cardinal ext-real positive non negative V183() V184() V185() V186() V187() V188() Element of NAT
TRm is V23() V27() V28() V29() finite cardinal ext-real non negative set
Seg TRm is finite TRm -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= TRm ) } is set
K19((Seg TRm)) is finite V38() set
A is V23() V27() V28() V29() finite cardinal ext-real non negative set

the carrier of () is non empty set

lines R is finite Element of K19( the carrier of ())
K19( the carrier of ()) is set
card () is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Mx2Tran R is Relation-like the carrier of (TOP-REAL TRm) -defined the carrier of () -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL TRm), the carrier of ()))

the carrier of (TOP-REAL TRm) is non empty set

the carrier of () is non empty set
K20( the carrier of (TOP-REAL TRm), the carrier of ()) is Relation-like set
K19(K20( the carrier of (TOP-REAL TRm), the carrier of ())) is set

x is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))

K20(NAT,( the carrier of F_Real *)) is Relation-like non empty V12() non finite set
K19(K20(NAT,( the carrier of F_Real *))) is non empty V12() non finite set
rng (R | x) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
K19(( the carrier of F_Real *)) is set
len R is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
width R is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Sum v is V28() V29() ext-real set
dom v is finite TRm -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)

Sum x is Relation-like Function-like Element of the carrier of ()
R is V23() V27() V28() V29() finite cardinal ext-real non negative set

() -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
x . (Line (R,R)) is set
{(Line (R,R))} is functional non empty V12() finite V38() 1 -element set
R " {(Line (R,R))} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)

dom (v | (R " {(Line (R,R))})) is finite set

(Sgm (dom (v | (R " {(Line (R,R))})))) (#) (v | (R " {(Line (R,R))})) is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued set
Sum (Seq (v | (R " {(Line (R,R))}))) is V28() V29() ext-real set
x is set
K19(()) is finite V38() set
{x} is non empty V12() finite 1 -element set
R is finite Element of K19(())
R " R is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
card (R " R) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
TRm -' (card (R " R)) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT

R ` is finite Element of K19(())
() \ R is finite Element of K19( the carrier of ())
R \/ (R `) is finite Element of K19(())
[#] () is finite Element of K19(())
R " (R `) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(R " R) \/ (R " (R `)) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
rng R is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
R " (rng R) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom R is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)

len C is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(len R) - (card (R " R)) is V28() V29() V30() V31() ext-real Element of INT
TRm - (card (R " R)) is V28() V29() ext-real Element of REAL
card (R " (R