:: 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
K876() is strict doubleLoopStr
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
K20(REAL,REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is non empty V12() non finite set
K20(K20(REAL,REAL),REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is non empty V12() non finite set
K20(RAT,RAT) is Relation-like RAT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is non empty V12() non finite set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is non empty V12() non finite set
K20(INT,INT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is non empty V12() non finite set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is non empty V12() non finite set
K20(NAT,NAT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued non empty V12() non finite complex-valued ext-real-valued real-valued natural-valued 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
REAL * is functional non empty FinSequence-membered FinSequenceSet of REAL
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
the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() V23() V27() V28() V29() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V177() decreasing non-decreasing non-increasing V183() V184() V185() V186() V187() V188() V189() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() V23() V27() V28() V29() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V177() decreasing non-decreasing non-increasing V183() V184() V185() V186() V187() V188() V189() 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
K20(K624(0,1,2),K624(0,1,2)) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K20(K20(K624(0,1,2),K624(0,1,2)),K624(0,1,2)) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued 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
K20(1,1) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20(1,1)) is finite V38() set
K20(K20(1,1),1) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(1,1),1)) is finite V38() set
K20(K20(1,1),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20(1,1),REAL)) is set
K20(2,2) is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K20(K20(2,2),REAL) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20(K20(2,2),REAL)) is set
TOP-REAL 2 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL 2) is non empty set
F_Real is non empty non degenerated V62() right_complementable almost_left_invertible strict Abelian add-associative right_zeroed V139() V141() V143() right-distributive left-distributive right_unital well-unital V149() left_unital doubleLoopStr
K143() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))
K145() is Relation-like K20(REAL,REAL) -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(K20(REAL,REAL),REAL))
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())
K20(NAT,REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
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)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= 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
<*> REAL is Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional empty V12() V23() V27() V28() V29() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V177() decreasing non-decreasing non-increasing V183() V184() V185() V186() V187() V188() V189() FinSequence of REAL
Sum (<*> REAL) is V28() V29() ext-real Element of REAL
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
REAL m is functional non empty FinSequence-membered FinSequenceSet of REAL
m -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
the carrier of (m -VectSp_over F_Real) is non empty set
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the carrier of (TOP-REAL m) is non empty set
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
m |-> (0. F_Real) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of m -tuples_on the carrier of F_Real
m -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
0* m is Relation-like NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL m
REAL m is functional non empty FinSequence-membered FinSequenceSet of REAL
m -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
m |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of m -tuples_on REAL
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
n is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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
@ n is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
@ (@ n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
m is set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (n -VectSp_over F_Real) is non empty set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
K19( the carrier of (n -VectSp_over F_Real)) is set
TRn is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of n -VectSp_over F_Real
TRm is finite Element of K19( the carrier of (n -VectSp_over F_Real))
A is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
TRn . A is set
Funcs ( the carrier of (TOP-REAL n),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (TOP-REAL n), REAL
K19( the carrier of (TOP-REAL n)) is set
TRn is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TOP-REAL n
TRm is finite Element of K19( the carrier of (TOP-REAL n))
A is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
TRn . A is V28() V29() ext-real set
Funcs ( the carrier of (n -VectSp_over F_Real), the carrier of F_Real) is functional non empty FUNCTION_DOMAIN of the carrier of (n -VectSp_over F_Real), the carrier of F_Real
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
MT is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Carrier MT is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
TRn is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TOP-REAL m
Carrier TRn is finite Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is set
TRm is set
A is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
R is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
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 (m -VectSp_over F_Real)
MT . A is V28() V29() ext-real Element of the carrier of F_Real
R is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K20( the carrier of (TOP-REAL m),REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (TOP-REAL m),REAL)) is non empty V12() non finite set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
K20( the carrier of (m -VectSp_over F_Real), the carrier of F_Real) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (m -VectSp_over F_Real), the carrier of F_Real)) is set
n is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
M is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (TOP-REAL m),REAL))
M (#) n is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
MT is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
TRn is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (m -VectSp_over F_Real), the carrier of F_Real))
TRn (#) MT is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
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
n /. A is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
m -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
MT /. A is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRm is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
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
R is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
M . R is V28() V29() ext-real set
(M . R) * R is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
v is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite m -element FinSequence-like FinSubsequence-like Element of m -tuples_on the carrier of F_Real
TRn . (MT /. A) is V28() V29() ext-real Element of the carrier of F_Real
(TRn . (MT /. A)) * v is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
(TRn . (MT /. A)) * (MT /. A) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
the lmult of (m -VectSp_over F_Real) is Relation-like K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like total quasi_total Element of K19(K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)))
K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)) is Relation-like set
K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)) is Relation-like set
K19(K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real))) is set
K329( the carrier of F_Real, the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real), the lmult of (m -VectSp_over F_Real),(TRn . (MT /. A)),(MT /. A)) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
(TRn (#) MT) . A is set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
MT is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
Sum MT is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
TRn is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
Sum TRn is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRm is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
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 (m -VectSp_over F_Real)) is Relation-like non empty V12() non finite set
K19(K20(NAT, the carrier of (m -VectSp_over F_Real))) 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
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
R is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like non empty total quasi_total Element of K19(K20(NAT, the carrier of (m -VectSp_over F_Real)))
R . (len TRn) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
R . 0 is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
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
m -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
TRn /. (v + 1) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
R . v is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
x is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite m -element FinSequence-like FinSubsequence-like Element of m -tuples_on the carrier of F_Real
@ x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
@ (@ x) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
R is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite m -element FinSequence-like FinSubsequence-like Element of m -tuples_on the carrier of F_Real
@ R is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
@ (@ R) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
MT /. (v + 1) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
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) + (@ x) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
R + x is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
(R . v) + (TRn /. (v + 1)) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
R . (v + 1) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
A . 0 is set
R . 0 is set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
MT is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Sum MT is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRn is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TOP-REAL m
Sum TRn is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
Carrier TRn is finite Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is set
TRm is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
rng TRm is finite Element of K19( the carrier of (TOP-REAL m))
TRn (#) TRm is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
Sum (TRn (#) TRm) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
A is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
MT (#) A is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
Carrier MT is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
Sum (MT (#) A) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
K19( the carrier of (m -VectSp_over F_Real)) is set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K19( the carrier of (TOP-REAL m)) is set
MT is Element of K19( the carrier of (m -VectSp_over F_Real))
Lin MT is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
[#] (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 (TOP-REAL m))
Lin TRn is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of TOP-REAL m
[#] (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
A is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TRn
Sum A is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
R is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Carrier R is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Carrier A is finite Element of K19( the carrier of (TOP-REAL m))
Sum R is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRm is set
A is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of MT
Sum A is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
R is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TOP-REAL m
Carrier R is finite Element of K19( the carrier of (TOP-REAL m))
Carrier A is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Sum R is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
K19( the carrier of (m -VectSp_over F_Real)) is set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K19( the carrier of (TOP-REAL m)) is set
M is Element of K19( the carrier of (m -VectSp_over F_Real))
TRn is Element of K19( the carrier of (TOP-REAL m))
TRm is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TRn
A is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Carrier A is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Carrier TRm is finite Element of K19( the carrier of (TOP-REAL m))
Sum TRm is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
Sum A is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRm is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of M
A is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TOP-REAL m
Carrier A is finite Element of K19( the carrier of (TOP-REAL m))
Carrier TRm is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Sum TRm is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
R is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TRn
Sum R is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
m is non empty non degenerated V62() right_complementable almost_left_invertible Abelian add-associative right_zeroed V139() V141() V143() right-distributive left-distributive right_unital well-unital V149() left_unital doubleLoopStr
the carrier of m is non empty V12() set
n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over m
the carrier of n is non empty set
M is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of M is non empty set
MT is Relation-like the carrier of n -defined the carrier of m -valued Function-like total quasi_total Linear_Combination of n
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
m is non empty non degenerated V62() right_complementable almost_left_invertible Abelian add-associative right_zeroed V139() V141() V143() right-distributive left-distributive right_unital well-unital V149() left_unital doubleLoopStr
the carrier of m is non empty V12() set
n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over m
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)
MT is Relation-like the carrier of n -defined the carrier of m -valued Function-like total quasi_total Linear_Combination of n
Carrier MT is finite Element of K19( the carrier 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
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
MT - TRn is Relation-like the carrier of n -defined the carrier of m -valued Function-like total quasi_total Linear_Combination 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)
ZeroLC n 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
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
m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of m is non empty set
n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of m
the carrier of n is non empty set
M is Relation-like the carrier of m -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of m
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)
(Carrier M) /\ the carrier of n is finite Element of K19( the carrier of m)
TRn is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of n,REAL)
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
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
TRn is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n -VectSp_over F_Real
[#] 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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of TOP-REAL n
[#] 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
A is Relation-like the carrier of TRn -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of TRn
R is finite Element of K19( the carrier of TRn)
A is Relation-like the carrier of TRm -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TRm
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
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
MT is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
the carrier of MT is non empty set
TRn is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of TOP-REAL m
the carrier of TRn is non empty set
TRm is Relation-like the carrier of MT -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of MT
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
A is Relation-like the carrier of TRn -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TRn
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 (TOP-REAL m) is non empty set
v is set
A . v is V28() V29() ext-real set
x is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
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
x is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
x is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
K20( the carrier of (TOP-REAL m),REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (TOP-REAL m),REAL)) is non empty V12() non finite set
v is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (TOP-REAL m),REAL))
K19( the carrier of (TOP-REAL m)) is set
Funcs ( the carrier of (TOP-REAL m),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (TOP-REAL m), REAL
x is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
x is finite Element of K19( the carrier of (TOP-REAL m))
A . x is V28() V29() ext-real set
v . x is V28() V29() ext-real Element of REAL
x is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TOP-REAL m
x | the carrier of TRn is Relation-like the carrier of TRn -defined the carrier of (TOP-REAL m) -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (TOP-REAL m),REAL))
L is set
x . L is V28() V29() ext-real set
A . L is V28() V29() ext-real set
R is Relation-like the carrier of TRn -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of TRn,REAL))
R . L is V28() V29() ext-real set
R is Relation-like the carrier of TRn -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of TRn,REAL))
R . L is V28() V29() ext-real set
the carrier of (m -VectSp_over F_Real) is non empty set
C is set
Carrier x is finite Element of K19( the carrier of (TOP-REAL m))
F is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
x . F is V28() V29() ext-real Element of REAL
A . F is V28() V29() ext-real set
Sum x is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
L is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Carrier L is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
Sum L is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
n is non empty non degenerated V62() right_complementable almost_left_invertible Abelian add-associative right_zeroed V139() V141() V143() right-distributive left-distributive right_unital well-unital V149() left_unital doubleLoopStr
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over n is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over n
the carrier of (m -VectSp_over n) is non empty set
K19( the carrier of (m -VectSp_over n)) is set
M is Element of K19( the carrier of (m -VectSp_over n))
Lin M is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over n
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
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,n, the carrier of F_Real
lines M is finite Element of K19( the carrier of (n -VectSp_over F_Real))
the carrier of (n -VectSp_over F_Real) is non empty set
K19( the carrier of (n -VectSp_over F_Real)) is set
Lin (lines M) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n -VectSp_over F_Real
[#] (Lin (lines M)) is non empty non proper Element of K19( the carrier of (Lin (lines M)))
the carrier of (Lin (lines M)) is non empty set
K19( the carrier of (Lin (lines M))) is set
MT is set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
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 (m -VectSp_over F_Real))
the carrier of (m -VectSp_over F_Real) is non empty set
K19( the carrier of (m -VectSp_over F_Real)) is set
Lin (lines M) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
the carrier of (Lin (lines M)) is non empty set
[#] (Lin (lines M)) is non empty non proper Element of K19( the carrier of (Lin (lines M)))
K19( the carrier of (Lin (lines M))) is set
MT is Element of K19( the carrier of (Lin (lines M)))
Lin MT is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of Lin (lines M)
TRn is Relation-like NAT -defined the carrier of (Lin (lines M)) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Lin (lines M))
m is non empty non degenerated V62() right_complementable almost_left_invertible Abelian add-associative right_zeroed V139() V141() V143() right-distributive left-distributive right_unital well-unital V149() left_unital doubleLoopStr
the carrier of m is non empty V12() set
n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over m
the carrier of n is non empty set
M is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over m
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))
TRm is Relation-like the carrier of n -defined the carrier of m -valued Function-like total quasi_total Linear_Combination of TRn
Sum TRm is Element of the carrier of n
MT . (Sum TRm) is Element of the carrier of M
MT @ TRm is Relation-like the carrier of M -defined the carrier of m -valued Function-like total quasi_total Linear_Combination of M
Sum (MT @ TRm) is Element of the carrier of M
Carrier TRm is finite Element of K19( the carrier of n)
A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
rng A is finite Element of K19( the carrier of n)
TRm (#) A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Sum (TRm (#) A) is Element of the carrier of n
MT * A is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
(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))
v is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of 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)
(MT @ TRm) (#) v is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
Sum ((MT @ TRm) (#) v) is Element of the carrier of M
MT * (TRm (#) A) is Relation-like NAT -defined the carrier of M -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of M
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) 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)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
M is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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)
MT is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
lines MT is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) 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 (TOP-REAL n) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)))
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m))) is set
(Mx2Tran MT) . M is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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
MT . v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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
Line (MT,x) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on the carrier of F_Real
(width MT) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
K20( the carrier of (m -VectSp_over F_Real), the carrier of F_Real) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (m -VectSp_over F_Real), the carrier of F_Real)) is set
x is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
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 is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (m -VectSp_over F_Real), the carrier of F_Real))
R . x is V28() V29() ext-real Element of the carrier of F_Real
Funcs ( the carrier of (m -VectSp_over F_Real), the carrier of F_Real) is functional non empty FUNCTION_DOMAIN of the carrier of (m -VectSp_over F_Real), the carrier of F_Real
C is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
L is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Element of Funcs ( the carrier of (m -VectSp_over F_Real), 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
TRn * (Line (MT,x)) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on 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
@ M is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
len (@ M) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
n -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
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)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
(Line (MT,x)) . F is set
F is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (MT,F) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on the carrier of F_Real
Col (MT,F) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite len MT -element FinSequence-like FinSubsequence-like Element of (len MT) -tuples_on the carrier of F_Real
(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)) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of n -tuples_on the carrier of F_Real
(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
mlt ((@ M),(Col (MT,F))) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
Sum (mlt ((@ M),(Col (MT,F)))) is V28() V29() ext-real Element of the carrier of F_Real
C is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite n -element FinSequence-like FinSubsequence-like Element of n -tuples_on the carrier of F_Real
(MT * (x,F)) * C is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
C is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Carrier C is finite Element of K19( the carrier of (m -VectSp_over F_Real))
{x} is functional non empty V12() finite 1 -element set
F is set
C . F is set
F is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines MT
Sum F is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
(1. F_Real) * x is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
the lmult of (m -VectSp_over F_Real) is Relation-like K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like total quasi_total Element of K19(K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)))
K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)) is Relation-like set
K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)) is Relation-like set
K19(K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real))) is set
K329( the carrier of F_Real, the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real), the lmult of (m -VectSp_over F_Real),(1. F_Real),x) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRn * F is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
F is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines MT
Sum F is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRn * (Sum F) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
K329( the carrier of F_Real, the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real), the lmult of (m -VectSp_over F_Real),TRn,(Sum F)) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
F is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (MT,F) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on the carrier of F_Real
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 * (1. F_Real) is V28() V29() ext-real Element of the carrier of F_Real
TRn * (1. F_Real) is V28() V29() ext-real Element of REAL
ZeroLC (m -VectSp_over F_Real) is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
TRn is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines MT
Sum TRn is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
TRm is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (MT,TRm) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on the carrier of F_Real
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
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) 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)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
K19((Seg n)) is finite V38() set
M is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
MT is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
lines MT is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
Mx2Tran MT is Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)))
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m))) is set
(Mx2Tran MT) . M is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= TRm ) } is set
K19((Seg TRm)) is finite V38() set
A is V23() V27() V28() V29() finite cardinal ext-real non negative set
A -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (A -VectSp_over F_Real) is non empty set
R is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of TRm,A, the carrier of F_Real
lines R is finite Element of K19( the carrier of (A -VectSp_over F_Real))
K19( the carrier of (A -VectSp_over F_Real)) is set
card (lines R) 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 (TOP-REAL A) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL TRm), the carrier of (TOP-REAL A)))
TOP-REAL TRm is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL TRm) is non empty set
TOP-REAL A is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL A) is non empty set
K20( the carrier of (TOP-REAL TRm), the carrier of (TOP-REAL A)) is Relation-like set
K19(K20( the carrier of (TOP-REAL TRm), the carrier of (TOP-REAL A))) is set
v is Relation-like NAT -defined Function-like finite TRm -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran R) . v is Relation-like NAT -defined Function-like finite A -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
x is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))
R | x is Relation-like NAT -defined x -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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)
x is Relation-like the carrier of (A -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines R
Sum x is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
R is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (R,R) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width R -element FinSequence-like FinSubsequence-like Element of (width R) -tuples_on the carrier of F_Real
(width R) -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)
v | (R " {(Line (R,R))}) is Relation-like NAT -defined R " {(Line (R,R))} -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
Seq (v | (R " {(Line (R,R))})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (v | (R " {(Line (R,R))})) is finite set
Sgm (dom (v | (R " {(Line (R,R))}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(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((lines R)) is finite V38() set
{x} is non empty V12() finite 1 -element set
R is finite Element of K19((lines R))
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 - R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R ` is finite Element of K19((lines R))
(lines R) \ R is finite Element of K19( the carrier of (A -VectSp_over F_Real))
R \/ (R `) is finite Element of K19((lines R))
[#] (lines R) is finite Element of K19((lines R))
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)
C is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of TRm -' (card (R " R)),A, the carrier of F_Real
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 `)) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(card (R " R)) + (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
card (dom 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 - (R `) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of TRm -' (card (R " (R `))),A, the carrier of F_Real
rng F is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
(rng R) \ (R `) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
(R `) ` is finite Element of K19((lines R))
len v is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
dom v is finite TRm -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom (R | x) is finite V183() V184() V185() V186() V187() V188() Element of K19(x)
K19(x) is finite V38() set
vAH is set
(R | x) . vAH is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R . vAH is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
h is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (R,h) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width R -element FinSequence-like FinSubsequence-like Element of (width R) -tuples_on the carrier of F_Real
(width R) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
len F 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
rng C is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
(rng R) \ R is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
card (rng C) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
card (rng R) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
card R is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(card (rng R)) - (card R) is V28() V29() V30() V31() ext-real Element of INT
(TRn + 1) - 1 is V28() V29() V30() V31() ext-real Element of INT
K20((dom R),(dom R)) is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((dom R),(dom R))) is finite V38() set
(R - R) ^ (R - (R `)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Hi is Relation-like dom R -defined dom R -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((dom R),(dom R)))
R * Hi is Relation-like dom R -defined the carrier of F_Real * -valued Function-like finite Element of K19(K20((dom R),( the carrier of F_Real *)))
K20((dom R),( the carrier of F_Real *)) is Relation-like set
K19(K20((dom R),( the carrier of F_Real *))) is set
K20((Seg TRm),(Seg TRm)) is Relation-like INT -valued RAT -valued finite complex-valued ext-real-valued real-valued natural-valued set
K19(K20((Seg TRm),(Seg TRm))) is finite V38() set
(R | x) * Hi is Relation-like dom R -defined the carrier of F_Real * -valued Function-like finite Element of K19(K20((dom R),( the carrier of F_Real *)))
j is Relation-like Seg TRm -defined Seg TRm -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg TRm),(Seg TRm)))
dom j is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))
j | (dom j) is Relation-like Seg TRm -defined dom j -defined Seg TRm -defined RAT -valued Seg TRm -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued Element of K19(K20((Seg TRm),(Seg TRm)))
(R | x) * (j | (dom j)) is Relation-like Seg TRm -defined the carrier of F_Real * -valued Function-like finite Element of K19(K20((Seg TRm),( the carrier of F_Real *)))
K20((Seg TRm),( the carrier of F_Real *)) is Relation-like set
K19(K20((Seg TRm),( the carrier of F_Real *))) is set
R * j is Relation-like NAT -defined Seg TRm -defined the carrier of F_Real * -valued the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of TRm,A, the carrier of F_Real
j " x is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))
(dom j) /\ (j " x) is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))
(R * j) | ((dom j) /\ (j " x)) is Relation-like NAT -defined (dom j) /\ (j " x) -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
(R * j) | (j " x) is Relation-like NAT -defined j " x -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
len (R * j) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
dom (R * j) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
J is Relation-like Function-like one-to-one set
J " is Relation-like Function-like one-to-one set
(J ") . h is set
rng j is finite V183() V184() V185() V186() V187() V188() Element of K19(REAL)
(J ") .: x is finite set
dom (J ") is set
j . ((J ") . h) is V23() V27() V28() V29() finite cardinal ext-real non negative set
dom C is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(R * Hi) . ((J ") . h) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R . h is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
C . ((J ") . h) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{((J ") . h)} is non empty V12() finite 1 -element set
(j " x) \ {((J ") . h)} is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))
hj1 is set
(R * j) . hj1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
j . hj1 is V23() V27() V28() V29() finite cardinal ext-real non negative set
R . (j . hj1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom Hi is finite V183() V184() V185() V186() V187() V188() Element of K19((dom R))
K19((dom R)) is finite V38() set
(R | x) . (j . hj1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(R | x) . h is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
dom F is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Hj1 is V23() V27() V28() V29() finite cardinal ext-real non negative set
vAHj1 is V23() V27() V28() V29() finite cardinal ext-real non negative set
(len C) + vAHj1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(R * j) . Hj1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F . vAHj1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(R * j) | ((j " x) \ {((J ") . h)}) is Relation-like NAT -defined (j " x) \ {((J ") . h)} -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
((R * j) | (j " x)) | ((j " x) \ {((J ") . h)}) is Relation-like NAT -defined (j " x) \ {((J ") . h)} -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
C | ((j " x) \ {((J ") . h)}) is Relation-like NAT -defined (j " x) \ {((J ") . h)} -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
(R | x) * j is Relation-like Seg TRm -defined the carrier of F_Real * -valued Function-like finite Element of K19(K20((Seg TRm),( the carrier of F_Real *)))
dom ((R | x) * j) is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))
((R | x) * j) . ((J ") . h) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
f is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
Im (((R | x) * j),((J ") . h)) is set
((R * j) | (j " x)) .: {((J ") . h)} is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
rng ((R * j) | (j " x)) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
(R * j) .: (j " x) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
((R * j) | (j " x)) .: (j " x) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
((R * j) | (j " x)) .: ((j " x) \ {((J ") . h)}) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
rng (((R * j) | (j " x)) | ((j " x) \ {((J ") . h)})) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
rng ((R * j) | ((j " x) \ {((J ") . h)})) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
rng (C | ((j " x) \ {((J ") . h)})) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
j (#) v is Relation-like Seg TRm -defined Function-like finite complex-valued ext-real-valued real-valued set
(TRm -' (card (R " R))) + (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
C ^ F is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `))))),A, the carrier of F_Real
K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `))))) is V23() V27() V28() V29() finite cardinal ext-real non negative set
len (C ^ F) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
hj1 is Relation-like NAT -defined REAL -valued Function-like finite TRm -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len hj1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Hj1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len Hj1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
vAHj1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len vAHj1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Hj1 ^ vAHj1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Mx2Tran F is Relation-like the carrier of (TOP-REAL (TRm -' (card (R " (R `))))) -defined the carrier of (TOP-REAL A) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL (TRm -' (card (R " (R `))))), the carrier of (TOP-REAL A)))
TOP-REAL (TRm -' (card (R " (R `)))) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL (TRm -' (card (R " (R `))))) is non empty set
K20( the carrier of (TOP-REAL (TRm -' (card (R " (R `))))), the carrier of (TOP-REAL A)) is Relation-like set
K19(K20( the carrier of (TOP-REAL (TRm -' (card (R " (R `))))), the carrier of (TOP-REAL A))) is set
(Mx2Tran F) . vAHj1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len ((Mx2Tran F) . vAHj1) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
lines F is finite Element of K19( the carrier of (A -VectSp_over F_Real))
Seg (TRm -' (card (R " (R `)))) is finite TRm -' (card (R " (R `))) -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= TRm -' (card (R " (R `))) ) } is set
Sum vAHj1 is V28() V29() ext-real Element of REAL
dom vAHj1 is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Fmj1 is Relation-like the carrier of (A -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines F
Sum Fmj1 is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
Mx2Tran C is Relation-like the carrier of (TOP-REAL (TRm -' (card (R " R)))) -defined the carrier of (TOP-REAL A) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL (TRm -' (card (R " R)))), the carrier of (TOP-REAL A)))
TOP-REAL (TRm -' (card (R " R))) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL (TRm -' (card (R " R)))) is non empty set
K20( the carrier of (TOP-REAL (TRm -' (card (R " R)))), the carrier of (TOP-REAL A)) is Relation-like set
K19(K20( the carrier of (TOP-REAL (TRm -' (card (R " R)))), the carrier of (TOP-REAL A))) is set
(Mx2Tran C) . Hj1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len ((Mx2Tran C) . Hj1) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
A -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
@ ((Mx2Tran C) . Hj1) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
@ ((Mx2Tran F) . vAHj1) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
Carrier Fmj1 is finite Element of K19( the carrier of (A -VectSp_over F_Real))
Seg (TRm -' (card (R " R))) is finite TRm -' (card (R " R)) -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b<sub>1</sub> where b<sub>1</sub> is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> <= TRm -' (card (R " R)) ) } is set
K19((Seg (TRm -' (card (R " R))))) is finite V38() set
lines C is finite Element of K19( the carrier of (A -VectSp_over F_Real))
L1 is Relation-like the carrier of (A -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines C
Sum L1 is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
Carrier L1 is finite Element of K19( the carrier of (A -VectSp_over F_Real))
(rng C) \/ (rng F) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
L1 + Fmj1 is Relation-like the carrier of (A -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of A -VectSp_over F_Real
L12 is Relation-like the carrier of (A -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines R
Sum L12 is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
Mx2Tran (C ^ F) is Relation-like the carrier of (TOP-REAL K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `)))))) -defined the carrier of (TOP-REAL A) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `)))))), the carrier of (TOP-REAL A)))
TOP-REAL K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `))))) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `)))))) is non empty set
K20( the carrier of (TOP-REAL K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `)))))), the carrier of (TOP-REAL A)) is Relation-like set
K19(K20( the carrier of (TOP-REAL K96((TRm -' (card (R " R))),(TRm -' (card (R " (R `)))))), the carrier of (TOP-REAL A))) is set
(Mx2Tran (C ^ F)) . (Hj1 ^ vAHj1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
((Mx2Tran C) . Hj1) + ((Mx2Tran F) . vAHj1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Mf1 is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite A -element FinSequence-like FinSubsequence-like Element of A -tuples_on the carrier of F_Real
Mf2 is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite A -element FinSequence-like FinSubsequence-like Element of A -tuples_on the carrier of F_Real
Mf1 + Mf2 is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
(Sum L1) + (Sum Fmj1) is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
w is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (R,w) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width R -element FinSequence-like FinSubsequence-like Element of (width R) -tuples_on the carrier of F_Real
L12 . (Line (R,w)) is set
{(Line (R,w))} is functional non empty V12() finite V38() 1 -element set
R " {(Line (R,w))} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
v | (R " {(Line (R,w))}) is Relation-like NAT -defined R " {(Line (R,w))} -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
Seq (v | (R " {(Line (R,w))})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (v | (R " {(Line (R,w))})) is finite set
Sgm (dom (v | (R " {(Line (R,w))}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (v | (R " {(Line (R,w))})))) (#) (v | (R " {(Line (R,w))})) is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued set
Sum (Seq (v | (R " {(Line (R,w))}))) is V28() V29() ext-real set
LMw is Relation-like Function-like Element of the carrier of (A -VectSp_over F_Real)
{LMw} is functional non empty V12() finite 1 -element set
R " {LMw} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
j " (R " {LMw}) is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRm))
(R * j) " {LMw} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
v | (R " {LMw}) is Relation-like NAT -defined R " {LMw} -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
Seq (v | (R " {LMw})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (v | (R " {LMw})) is finite set
Sgm (dom (v | (R " {LMw}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (v | (R " {LMw})))) (#) (v | (R " {LMw})) is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued set
Sum (Seq (v | (R " {LMw}))) is V28() V29() ext-real set
hj1 | ((R * j) " {LMw}) is Relation-like NAT -defined (R * j) " {LMw} -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Seq (hj1 | ((R * j) " {LMw})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (hj1 | ((R * j) " {LMw})) is finite set
Sgm (dom (hj1 | ((R * j) " {LMw}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (hj1 | ((R * j) " {LMw})))) (#) (hj1 | ((R * j) " {LMw})) is Relation-like NAT -defined REAL -valued Function-like finite complex-valued ext-real-valued real-valued set
Sum (Seq (hj1 | ((R * j) " {LMw}))) is V28() V29() ext-real set
C " {LMw} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Hj1 | (C " {LMw}) is Relation-like NAT -defined C " {LMw} -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Seq (Hj1 | (C " {LMw})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (Hj1 | (C " {LMw})) is finite set
Sgm (dom (Hj1 | (C " {LMw}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (Hj1 | (C " {LMw})))) (#) (Hj1 | (C " {LMw})) is Relation-like NAT -defined REAL -valued Function-like finite complex-valued ext-real-valued real-valued set
F " {LMw} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
vAHj1 | (F " {LMw}) is Relation-like NAT -defined F " {LMw} -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
Seq (vAHj1 | (F " {LMw})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (vAHj1 | (F " {LMw})) is finite set
Sgm (dom (vAHj1 | (F " {LMw}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (vAHj1 | (F " {LMw})))) (#) (vAHj1 | (F " {LMw})) is Relation-like NAT -defined REAL -valued Function-like finite complex-valued ext-real-valued real-valued set
(Seq (Hj1 | (C " {LMw}))) ^ (Seq (vAHj1 | (F " {LMw}))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Sum ((Seq (Hj1 | (C " {LMw}))) ^ (Seq (vAHj1 | (F " {LMw})))) is V28() V29() ext-real set
Sum (Seq (Hj1 | (C " {LMw}))) is V28() V29() ext-real set
Sum (Seq (vAHj1 | (F " {LMw}))) is V28() V29() ext-real set
(Sum (Seq (Hj1 | (C " {LMw})))) + (Sum (Seq (vAHj1 | (F " {LMw})))) is V28() V29() ext-real Element of REAL
(J ") . w is set
j . ((J ") . w) is V23() V27() V28() V29() finite cardinal ext-real non negative set
(R * Hi) . ((J ") . w) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
R . w is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F is non empty non degenerated V62() right_complementable almost_left_invertible Abelian add-associative right_zeroed V139() V141() V143() right-distributive left-distributive right_unital well-unital V149() left_unital doubleLoopStr
the carrier of F is non empty V12() set
L1 . LMw is V28() V29() ext-real Element of the carrier of F_Real
Fmj1 . LMw is V28() V29() ext-real Element of the carrier of F_Real
L12 . LMw is V28() V29() ext-real Element of the carrier of F_Real
L1w is Element of the carrier of F
L2w is Element of the carrier of F
L1w + L2w is Element of the carrier of F
ppw is V23() V27() V28() V29() finite cardinal ext-real non negative set
C . ppw is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (C,ppw) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width C -element FinSequence-like FinSubsequence-like Element of (width C) -tuples_on the carrier of F_Real
width C is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(width C) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
dom F is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
ppw is V23() V27() V28() V29() finite cardinal ext-real non negative set
z is V23() V27() V28() V29() finite cardinal ext-real non negative set
(len C) + z is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
z is V23() V27() V28() V29() finite cardinal ext-real non negative set
(len C) + z is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
F . z is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
L2w + L1w is Element of the carrier of F
Line (F,z) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width F -element FinSequence-like FinSubsequence-like Element of (width F) -tuples_on the carrier of F_Real
width F is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(width F) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
ppw is V23() V27() V28() V29() finite cardinal ext-real non negative set
dom F is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
TRn is V23() V27() V28() V29() finite cardinal ext-real non negative set
Seg TRn is finite TRn -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= TRn ) } is set
K19((Seg TRn)) is finite V38() set
TRm is V23() V27() V28() V29() finite cardinal ext-real non negative set
TRm -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (TRm -VectSp_over F_Real) is non empty set
A is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of TRn,TRm, the carrier of F_Real
lines A is finite Element of K19( the carrier of (TRm -VectSp_over F_Real))
K19( the carrier of (TRm -VectSp_over F_Real)) is set
card (lines A) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Mx2Tran A is Relation-like the carrier of (TOP-REAL TRn) -defined the carrier of (TOP-REAL TRm) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL TRn), the carrier of (TOP-REAL TRm)))
TOP-REAL TRn is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL TRn) is non empty set
TOP-REAL TRm is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL TRm) is non empty set
K20( the carrier of (TOP-REAL TRn), the carrier of (TOP-REAL TRm)) is Relation-like set
K19(K20( the carrier of (TOP-REAL TRn), the carrier of (TOP-REAL TRm))) is set
R is Relation-like NAT -defined Function-like finite TRn -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran A) . R is Relation-like NAT -defined Function-like finite TRm -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
v is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRn))
A | v is Relation-like NAT -defined v -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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 (A | v) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
K19(( the carrier of F_Real *)) is set
ZeroLC (TRm -VectSp_over F_Real) is Relation-like the carrier of (TRm -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of TRm -VectSp_over F_Real
x is Relation-like the carrier of (TRm -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines A
Sum x is Relation-like Function-like Element of the carrier of (TRm -VectSp_over F_Real)
0. (TRm -VectSp_over F_Real) is Relation-like Function-like V64(TRm -VectSp_over F_Real) Element of the carrier of (TRm -VectSp_over F_Real)
the ZeroF of (TRm -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (TRm -VectSp_over F_Real)
0. (TOP-REAL TRm) is Relation-like NAT -defined Function-like finite TRm -element FinSequence-like FinSubsequence-like V64( TOP-REAL TRm) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL TRm)
the ZeroF of (TOP-REAL TRm) is Relation-like NAT -defined Function-like finite TRm -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL TRm)
len A 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
Line (A,x) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width A -element FinSequence-like FinSubsequence-like Element of (width A) -tuples_on the carrier of F_Real
width A is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(width A) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
x . (Line (A,x)) is set
{(Line (A,x))} is functional non empty V12() finite V38() 1 -element set
A " {(Line (A,x))} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
R | (A " {(Line (A,x))}) is Relation-like NAT -defined A " {(Line (A,x))} -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
Seq (R | (A " {(Line (A,x))})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (R | (A " {(Line (A,x))})) is finite set
Sgm (dom (R | (A " {(Line (A,x))}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (R | (A " {(Line (A,x))})))) (#) (R | (A " {(Line (A,x))})) is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued set
Sum (Seq (R | (A " {(Line (A,x))}))) is V28() V29() ext-real 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
TRn is V23() V27() V28() V29() finite cardinal ext-real non negative set
TRm is V23() V27() V28() V29() finite cardinal ext-real non negative set
Seg TRn is finite TRn -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= TRn ) } is set
K19((Seg TRn)) is finite V38() set
A is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of TRn,TRm, the carrier of F_Real
v is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg TRn))
A | v is Relation-like NAT -defined v -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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 (A | v) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
K19(( the carrier of F_Real *)) is set
lines A is finite Element of K19( the carrier of (TRm -VectSp_over F_Real))
TRm -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (TRm -VectSp_over F_Real) is non empty set
K19( the carrier of (TRm -VectSp_over F_Real)) is set
card (lines A) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Mx2Tran A is Relation-like the carrier of (TOP-REAL TRn) -defined the carrier of (TOP-REAL TRm) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL TRn), the carrier of (TOP-REAL TRm)))
TOP-REAL TRn is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL TRn) is non empty set
TOP-REAL TRm is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL TRm) is non empty set
K20( the carrier of (TOP-REAL TRn), the carrier of (TOP-REAL TRm)) is Relation-like set
K19(K20( the carrier of (TOP-REAL TRn), the carrier of (TOP-REAL TRm))) is set
R is Relation-like NAT -defined Function-like finite TRn -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran A) . R is Relation-like NAT -defined Function-like finite TRm -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
TRn is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg n))
MT | TRn is Relation-like NAT -defined TRn -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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 (MT | TRn) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
K19(( the carrier of F_Real *)) is set
TRn is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg n))
MT | TRn is Relation-like NAT -defined TRn -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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 (MT | TRn) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
K19(( the carrier of F_Real *)) is set
ZeroLC (m -VectSp_over F_Real) is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
TRm is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines MT
Sum TRm is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
A is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (MT,A) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on the carrier of F_Real
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
TRm . (Line (MT,A)) is set
{(Line (MT,A))} is functional non empty V12() finite V38() 1 -element set
MT " {(Line (MT,A))} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
M | (MT " {(Line (MT,A))}) is Relation-like NAT -defined MT " {(Line (MT,A))} -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
Seq (M | (MT " {(Line (MT,A))})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (M | (MT " {(Line (MT,A))})) is finite set
Sgm (dom (M | (MT " {(Line (MT,A))}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (M | (MT " {(Line (MT,A))})))) (#) (M | (MT " {(Line (MT,A))})) is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued set
Sum (Seq (M | (MT " {(Line (MT,A))}))) is V28() V29() ext-real 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
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (n -VectSp_over F_Real) is non empty set
M is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom M is finite m -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
MT is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,n, the carrier of F_Real
lines MT is finite Element of K19( the carrier of (n -VectSp_over F_Real))
K19( the carrier of (n -VectSp_over F_Real)) is set
Mx2Tran MT is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL n) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n)))
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n)) is Relation-like set
K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n))) is set
(Mx2Tran MT) . M is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued 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
dom MT is finite 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)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
K19((Seg m)) is finite V38() set
len M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
MT | (dom MT) is Relation-like NAT -defined dom MT -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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
TRn is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg m))
TRm is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines MT
Sum TRm is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
A is V23() V27() V28() V29() finite cardinal ext-real non negative set
Line (MT,A) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on the carrier of F_Real
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
TRm . (Line (MT,A)) is set
M . A is V28() V29() ext-real set
{A} is non empty V12() finite V38() 1 -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Sgm {A} is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
<*A*> is Relation-like NAT -defined Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V177() decreasing non-decreasing non-increasing set
[1,A] is non empty set
{1,A} is finite V38() V183() V184() V185() V186() V187() V188() set
{1} is non empty V12() finite V38() 1 -element V183() V184() V185() V186() V187() V188() set
{{1,A},{1}} is finite V38() set
{[1,A]} is Relation-like Function-like constant non empty V12() finite 1 -element set
{(Line (MT,A))} is functional non empty V12() finite V38() 1 -element set
MT " {(Line (MT,A))} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
v is set
{v} is non empty V12() finite 1 -element set
M | {A} is Relation-like NAT -defined {A} -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (M | {A}) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(dom M) /\ {A} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(M | {A}) . A is V28() V29() ext-real set
rng <*A*> is non empty V12() finite 1 -element V183() V184() V185() Element of K19(REAL)
rng (M | {A}) is finite V183() V184() V185() Element of K19(REAL)
K20({A},(rng (M | {A}))) is Relation-like finite complex-valued ext-real-valued real-valued set
K19(K20({A},(rng (M | {A})))) is finite V38() set
Seq (M | {A}) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (M | {A}) is finite set
Sgm (dom (M | {A})) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (M | {A}))) (#) (M | {A}) is Relation-like NAT -defined Function-like finite complex-valued ext-real-valued real-valued set
<*(M . A)*> is Relation-like NAT -defined Function-like one-to-one constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued V177() decreasing non-decreasing non-increasing set
[1,(M . A)] is non empty set
{1,(M . A)} is finite V183() V184() V185() set
{{1,(M . A)},{1}} is finite V38() set
{[1,(M . A)]} is Relation-like Function-like constant non empty V12() finite 1 -element set
Sum (Seq (M | {A})) is V28() V29() ext-real set
MT . A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
M | (MT " {(Line (MT,A))}) is Relation-like NAT -defined MT " {(Line (MT,A))} -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued 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
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
M is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
MT is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,n, the carrier of F_Real
lines MT is finite Element of K19( the carrier of (n -VectSp_over F_Real))
the carrier of (n -VectSp_over F_Real) is non empty set
K19( the carrier of (n -VectSp_over F_Real)) is set
Lin (lines MT) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n -VectSp_over F_Real
the carrier of (Lin (lines MT)) is non empty set
Mx2Tran MT is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL n) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n)))
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n)) is Relation-like set
K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n))) is set
(Mx2Tran MT) . M is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
TRm is Relation-like NAT -defined the carrier of (Lin (lines MT)) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of Lin (lines MT)
A is Element of the carrier of (Lin (lines MT))
A |-- TRm is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
dom M is finite m -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
R is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines MT
Sum R is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
R | the carrier of (Lin (lines MT)) is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of (Lin (lines MT)) -defined the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of F_Real))
K20( the carrier of (n -VectSp_over F_Real), the carrier of F_Real) is Relation-like complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of F_Real)) 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 M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
[#] (Lin (lines MT)) is non empty non proper Element of K19( the carrier of (Lin (lines MT)))
K19( the carrier of (Lin (lines MT))) is set
x is V23() V27() V28() V29() finite cardinal ext-real non negative set
Seg m is finite m -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
MT . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (MT,x) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width MT -element FinSequence-like FinSubsequence-like Element of (width MT) -tuples_on the carrier of F_Real
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
dom MT is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
TRm /. x is Element of the carrier of (Lin (lines MT))
R . (MT . x) is set
v is Relation-like the carrier of (Lin (lines MT)) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of Lin (lines MT)
v . (MT . x) is set
M . x is V28() V29() ext-real set
@ M is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
(@ M) /. x is V28() V29() ext-real Element of the carrier of F_Real
v . (TRm /. x) is V28() V29() ext-real Element of the carrier of F_Real
Carrier R is finite Element of K19( the carrier of (n -VectSp_over F_Real))
Carrier v is finite Element of K19( the carrier of (Lin (lines MT)))
Sum v is Element of the carrier of (Lin (lines MT))
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
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,n, the carrier of F_Real
Mx2Tran M is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL n) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n)))
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n)) is Relation-like set
K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL n))) is set
rng (Mx2Tran M) is non empty Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is set
lines M is finite Element of K19( the carrier of (n -VectSp_over F_Real))
the carrier of (n -VectSp_over F_Real) is non empty set
K19( the carrier of (n -VectSp_over F_Real)) is set
Lin (lines M) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n -VectSp_over F_Real
[#] (Lin (lines M)) is non empty non proper Element of K19( the carrier of (Lin (lines M)))
the carrier of (Lin (lines M)) is non empty set
K19( the carrier of (Lin (lines M))) is set
dom M is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
MT is set
M | MT is Relation-like NAT -defined MT -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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 (M | MT) is functional finite FinSequence-membered Element of K19(( the carrier of F_Real *))
K19(( the carrier of F_Real *)) is set
len M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Seg m is finite m -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= m ) } is set
K19((Seg m)) is finite V38() set
R is set
dom (Mx2Tran M) is non empty Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is set
v is set
(Mx2Tran M) . v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
A is finite V183() V184() V185() V186() V187() V188() Element of K19((Seg m))
x is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
x is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines M
Sum x is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
R is set
v is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines M
Sum v is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
x is V23() V27() V28() V29() finite cardinal ext-real non negative set
M . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v . (M . x) is set
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom x is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
rng x is finite set
x is set
R is set
x . R is set
L is V23() V27() V28() V29() finite cardinal ext-real non negative set
x . L is set
M . L is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
v . (M . L) is set
Line (M,L) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width M -element FinSequence-like FinSubsequence-like Element of (width M) -tuples_on the carrier of F_Real
width M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(width M) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len x is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(Mx2Tran M) . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
R is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of lines M
Sum R is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
L is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
M | A is Relation-like NAT -defined A -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
dom (M | A) is finite V183() V184() V185() V186() V187() V188() Element of K19(A)
K19(A) is finite V38() set
C is set
(M | A) . C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
M . C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
{L} is functional non empty V12() finite 1 -element set
M " {L} is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
x | (M " {L}) is Relation-like NAT -defined M " {L} -defined NAT -defined REAL -valued Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
dom (x | (M " {L})) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Seq (x | (M " {L})) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom (x | (M " {L})) is finite set
Sgm (dom (x | (M " {L}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
(Sgm (dom (x | (M " {L})))) (#) (x | (M " {L})) is Relation-like NAT -defined REAL -valued Function-like finite complex-valued ext-real-valued real-valued set
@ (Seq (x | (M " {L}))) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
@ (@ (Seq (x | (M " {L})))) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sgm (dom (x | (M " {L}))) is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued FinSequence of NAT
rng (Sgm (dom (x | (M " {L})))) is finite V183() V184() V185() V186() V187() V188() Element of K19(REAL)
F is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom F is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom (Sgm (dom (x | (M " {L})))) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
F is V23() V27() V28() V29() finite cardinal ext-real non negative set
M . F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Line (M,F) is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite width M -element FinSequence-like FinSubsequence-like Element of (width M) -tuples_on the carrier of F_Real
width M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(width M) -tuples_on the carrier of F_Real is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
R . L is V28() V29() ext-real Element of the carrier of F_Real
Sum (Seq (x | (M " {L}))) is V28() V29() ext-real set
Fm is set
(Sgm (dom (x | (M " {L})))) . Fm is V23() V27() V28() V29() finite cardinal ext-real non negative set
fm is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
F . fm is V28() V29() ext-real set
(x | (M " {L})) . F is V28() V29() ext-real set
x . F is V28() V29() ext-real set
dom x is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
vAH is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(Sgm (dom (x | (M " {L})))) . vAH is V23() V27() V28() V29() finite cardinal ext-real non negative set
M . ((Sgm (dom (x | (M " {L})))) . vAH) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(M | A) . ((Sgm (dom (x | (M " {L})))) . vAH) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F . vAH is V28() V29() ext-real set
(x | (M " {L})) . ((Sgm (dom (x | (M " {L})))) . vAH) is V28() V29() ext-real set
x . ((Sgm (dom (x | (M " {L})))) . vAH) is V28() V29() ext-real set
v . L is V28() V29() ext-real Element of the carrier of F_Real
L is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
Carrier v is finite Element of K19( the carrier of (n -VectSp_over F_Real))
v . L is V28() V29() ext-real Element of the carrier of F_Real
Carrier R is finite Element of K19( the carrier of (n -VectSp_over F_Real))
R . L is V28() V29() ext-real Element of the carrier of F_Real
L is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
[#] (TOP-REAL m) is non empty non proper Element of K19( the carrier of (TOP-REAL m))
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
n is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
rng n is finite Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is 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 -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
M is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
FinS2MX M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len M,m, the carrier of F_Real
len M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
lines (FinS2MX M) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
the_rank_of (FinS2MX M) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
m -' (len n) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
TRn is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m -' (len n),m, the carrier of F_Real
(FinS2MX M) ^ TRn is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K96((len M),(m -' (len n))),m, the carrier of F_Real
K96((len M),(m -' (len n))) is V23() V27() V28() V29() finite cardinal ext-real non negative set
the_rank_of ((FinS2MX M) ^ TRn) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
width (FinS2MX M) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
m - (len n) is V28() V29() ext-real Element of REAL
TRm is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
TRm | (len n) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Real *
Seg (len n) is finite len n -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
TRm | (Seg (len n)) is Relation-like NAT -defined Seg (len n) -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like set
Det TRm is V28() V29() ext-real Element of the carrier of F_Real
dom n is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
TRm | (dom n) is Relation-like NAT -defined dom n -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT,( the carrier of F_Real *)))
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
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
1. (F_Real,m) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
MX2FinS (1. (F_Real,m)) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
m -' n is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(m -' n) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite m -' n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of (m -' n) -tuples_on NAT
(m -' n) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
M is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
M | n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg n is finite n -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
M | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
(M | n) ^ ((m -' n) |-> 0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
TRm is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of m -VectSp_over F_Real
TRm | n is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
TRm | (Seg n) is Relation-like NAT -defined Seg n -defined NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSubsequence-like set
rng (TRm | n) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
Lin (rng (TRm | n)) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
len TRm is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
rng TRm is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Lin (rng TRm) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
the addF of (m -VectSp_over F_Real) is Relation-like K20( the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like total quasi_total Element of K19(K20(K20( the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)))
K20( the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)) is Relation-like set
K20(K20( the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)) is Relation-like set
K19(K20(K20( the carrier of (m -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real))) is set
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
the lmult of (m -VectSp_over F_Real) is Relation-like K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like total quasi_total Element of K19(K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)))
K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)) is Relation-like set
K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real)) is Relation-like set
K19(K20(K20( the carrier of F_Real, the carrier of (m -VectSp_over F_Real)), the carrier of (m -VectSp_over F_Real))) is set
VectSpStr(# the carrier of (m -VectSp_over F_Real), the addF of (m -VectSp_over F_Real), the ZeroF of (m -VectSp_over F_Real), the lmult of (m -VectSp_over F_Real) #) is non empty strict VectSpStr over F_Real
len M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
m - n is V28() V29() ext-real Element of REAL
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 ((m -' n) |-> 0) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
A is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
A |-- TRm is Relation-like NAT -defined the carrier of F_Real -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of the carrier of F_Real
len (A |-- TRm) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
R is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Sum R is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
Carrier R is finite Element of K19( the carrier of (m -VectSp_over F_Real))
m - n is V28() V29() ext-real Element of REAL
len ((M | n) ^ ((m -' n) |-> 0)) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
n + (m - n) is V28() V29() ext-real Element of REAL
dom ((M | n) ^ ((m -' n) |-> 0)) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom M is finite m -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
x is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of rng (TRm | n)
Sum x is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
v is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of rng TRm
x is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of rng TRm
v - x is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Sum (v - x) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
Sum v is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
Sum x is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
(Sum v) - (Sum x) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
Carrier (v - x) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
ZeroLC (m -VectSp_over F_Real) is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
- x is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
v + (- x) is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
(- x) + v is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
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
- (1. F_Real) is V28() V29() ext-real Element of REAL
Carrier x is finite Element of K19( the carrier of (m -VectSp_over F_Real))
- (- x) is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
L is V23() V27() V28() V29() finite cardinal ext-real non negative set
dom (M | n) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(M | n) . L is set
M . L is V28() V29() ext-real set
((M | n) ^ ((m -' n) |-> 0)) . L is set
dom ((m -' n) |-> 0) is finite m -' n -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom TRm is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
TRm /. L is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRm . L is set
C is V23() V27() V28() V29() finite cardinal ext-real non negative set
n + C is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
C is V23() V27() V28() V29() finite cardinal ext-real non negative set
n + C is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
dom (TRm | n) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
F is set
(TRm | n) . F is set
TRm . F is set
n + 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 |-- TRm) /. L is V28() V29() ext-real Element of the carrier of F_Real
v . (TRm /. L) is V28() V29() ext-real Element of the carrier of F_Real
M . L is V28() V29() ext-real set
((m -' n) |-> 0) . C is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() V23() V27() V28() V29() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V177() decreasing non-decreasing non-increasing V183() V184() V185() V186() V187() V188() V189() set
((M | n) ^ ((m -' n) |-> 0)) . L is set
dom (M | n) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom ((m -' n) |-> 0) is finite m -' n -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Carrier v is finite Element of K19( the carrier of (m -VectSp_over F_Real))
x is set
dom TRm is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
x is set
TRm . x is set
R is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
TRm /. R is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
TRm . R is set
dom (TRm | n) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(TRm | n) . R is set
dom (M | n) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
dom ((m -' n) |-> 0) is finite m -' n -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
L is V23() V27() V28() V29() finite cardinal ext-real non negative set
n + L is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
((m -' n) |-> 0) . L is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() V23() V27() V28() V29() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V177() decreasing non-decreasing non-increasing V183() V184() V185() V186() V187() V188() V189() set
(A |-- TRm) /. R is V28() V29() ext-real Element of the carrier of F_Real
(A |-- TRm) . R is V28() V29() ext-real set
v . (TRm /. R) is V28() V29() ext-real Element of the carrier of F_Real
M . R is V28() V29() ext-real set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
1. (F_Real,m) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
MX2FinS (1. (F_Real,m)) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
n is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
rng n is finite Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is 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
Lin (rng n) is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of TOP-REAL m
[#] (Lin (rng n)) is non empty non proper Element of K19( the carrier of (Lin (rng n)))
the carrier of (Lin (rng n)) is non empty set
K19( the carrier of (Lin (rng n))) is set
M is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
FinS2MX M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len M,m, the carrier of F_Real
len M is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
m -' (len n) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
lines (FinS2MX M) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
the_rank_of (FinS2MX M) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
width (FinS2MX M) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
m - (len n) is V28() V29() ext-real Element of REAL
R is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of m -VectSp_over F_Real
R | (len n) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
Seg (len n) is finite len n -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
R | (Seg (len n)) is Relation-like NAT -defined Seg (len n) -defined NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSubsequence-like set
rng (R | (len n)) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Lin (rng (R | (len n))) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
[#] (Lin (rng (R | (len n)))) is non empty non proper Element of K19( the carrier of (Lin (rng (R | (len n)))))
the carrier of (Lin (rng (R | (len n)))) is non empty set
K19( the carrier of (Lin (rng (R | (len n))))) is set
v is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
v | (len n) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Real *
v | (Seg (len n)) is Relation-like NAT -defined Seg (len n) -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like set
Mx2Tran v is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)))
K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m))) is set
(Mx2Tran v) .: ([#] (Lin (rng (R | (len n))))) is Element of K19( the carrier of (TOP-REAL m))
x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
n ^ x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
MX2FinS v is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
len v is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
x is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
len x is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(len n) + (len x) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
FinS2MX x is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len x,m, the carrier of F_Real
dom (Mx2Tran v) is non empty Element of K19( the carrier of (TOP-REAL m))
[#] (TOP-REAL m) is non empty non proper Element of K19( the carrier of (TOP-REAL m))
TOP-REAL (len M) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL (len M)) is non empty set
Mx2Tran (FinS2MX M) is Relation-like the carrier of (TOP-REAL (len M)) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL (len M)), the carrier of (TOP-REAL m)))
K20( the carrier of (TOP-REAL (len M)), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL (len M)), the carrier of (TOP-REAL m))) is set
dom (Mx2Tran (FinS2MX M)) is non empty Element of K19( the carrier of (TOP-REAL (len M)))
K19( the carrier of (TOP-REAL (len M))) is set
TOP-REAL (len n) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
[#] (TOP-REAL (len n)) is non empty non proper Element of K19( the carrier of (TOP-REAL (len n)))
the carrier of (TOP-REAL (len n)) is non empty set
K19( the carrier of (TOP-REAL (len n))) is set
REAL m is functional non empty FinSequence-membered FinSequenceSet of REAL
m -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
rng (Mx2Tran (FinS2MX M)) is non empty Element of K19( the carrier of (TOP-REAL m))
Lin (lines (FinS2MX M)) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
[#] (Lin (lines (FinS2MX M))) is non empty non proper Element of K19( the carrier of (Lin (lines (FinS2MX M))))
the carrier of (Lin (lines (FinS2MX M))) is non empty set
K19( the carrier of (Lin (lines (FinS2MX M)))) is set
m |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of m -tuples_on NAT
m -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
0* m is Relation-like NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL m
m |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of m -tuples_on REAL
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(m -' (len n)) |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite m -' (len n) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Element of (m -' (len n)) -tuples_on NAT
(m -' (len n)) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
0* (m -' (len n)) is Relation-like NAT -defined REAL -valued Function-like finite m -' (len n) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of REAL (m -' (len n))
REAL (m -' (len n)) is functional non empty FinSequence-membered FinSequenceSet of REAL
(m -' (len n)) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
(m -' (len n)) |-> 0 is Relation-like empty-yielding NAT -defined REAL -valued Function-like finite m -' (len n) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (m -' (len n)) -tuples_on REAL
TOP-REAL (m -' (len n)) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
0. (TOP-REAL (m -' (len n))) is Relation-like NAT -defined Function-like finite m -' (len n) -element FinSequence-like FinSubsequence-like V64( TOP-REAL (m -' (len n))) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL (m -' (len n)))
the carrier of (TOP-REAL (m -' (len n))) is non empty set
the ZeroF of (TOP-REAL (m -' (len n))) is Relation-like NAT -defined Function-like finite m -' (len n) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL (m -' (len n)))
Mx2Tran (FinS2MX x) is Relation-like the carrier of (TOP-REAL (len x)) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL (len x)), the carrier of (TOP-REAL m)))
TOP-REAL (len x) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL (len x)) is non empty set
K20( the carrier of (TOP-REAL (len x)), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL (len x)), the carrier of (TOP-REAL m))) is set
(Mx2Tran (FinS2MX x)) . ((m -' (len n)) |-> 0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
C is set
F is set
(Mx2Tran v) . F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
F is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
len F is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
F | (len n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
F | (Seg (len n)) is Relation-like NAT -defined Seg (len n) -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
len (F | (len n)) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(Mx2Tran (FinS2MX M)) . (F | (len n)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(F | (len n)) ^ ((m -' (len n)) |-> 0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
((Mx2Tran (FinS2MX M)) . (F | (len n))) + ((Mx2Tran (FinS2MX x)) . ((m -' (len n)) |-> 0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
C is set
F is set
(Mx2Tran (FinS2MX M)) . F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
F is Relation-like NAT -defined Function-like finite len n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL (len n))
(Mx2Tran (FinS2MX M)) . F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
((Mx2Tran (FinS2MX M)) . F) + (0. (TOP-REAL m)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
((Mx2Tran (FinS2MX M)) . F) + ((Mx2Tran (FinS2MX x)) . ((m -' (len n)) |-> 0)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
F ^ ((m -' (len n)) |-> 0) is Relation-like NAT -defined Function-like finite K412((len n),(m -' (len n))) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
K412((len n),(m -' (len n))) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
(Mx2Tran v) . (F ^ ((m -' (len n)) |-> 0)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
len F is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
dom F is finite len n -element V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(F ^ ((m -' (len n)) |-> 0)) | (len n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(F ^ ((m -' (len n)) |-> 0)) | (Seg (len n)) is Relation-like NAT -defined Seg (len n) -defined NAT -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued set
((F ^ ((m -' (len n)) |-> 0)) | (len n)) ^ ((m -' (len n)) |-> 0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K19( the carrier of (TOP-REAL m)) is set
M is affinely-independent linearly-independent Element of K19( the carrier of (TOP-REAL m))
card M is V23() cardinal set
MT is affinely-independent linearly-independent Element of K19( the carrier of (TOP-REAL m))
card MT is V23() cardinal set
Lin M is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of TOP-REAL m
[#] (Lin M) is non empty non proper Element of K19( the carrier of (Lin M))
the carrier of (Lin M) is non empty set
K19( the carrier of (Lin M)) is set
Lin MT is non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of TOP-REAL m
[#] (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
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
1. (F_Real,m) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
MX2FinS (1. (F_Real,m)) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
K19( the carrier of (m -VectSp_over F_Real)) is set
A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng A is finite set
len A is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng R is finite 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
v is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
len v is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
x is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
x | (len v) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Real *
Seg (len v) is finite len v -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= len v ) } is set
x | (Seg (len v)) is Relation-like NAT -defined Seg (len v) -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like set
TRn is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of m -VectSp_over F_Real
TRn | (len v) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
TRn | (Seg (len v)) is Relation-like NAT -defined Seg (len v) -defined NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSubsequence-like set
rng (TRn | (len v)) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Lin (rng (TRn | (len v))) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
[#] (Lin (rng (TRn | (len v)))) is non empty non proper Element of K19( the carrier of (Lin (rng (TRn | (len v)))))
the carrier of (Lin (rng (TRn | (len v)))) is non empty set
K19( the carrier of (Lin (rng (TRn | (len v))))) is set
[#] (m -VectSp_over F_Real) is non empty non proper Element of K19( the carrier of (m -VectSp_over F_Real))
Mx2Tran x is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)))
K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m))) is set
Det x is V28() V29() ext-real Element of the carrier of F_Real
(Mx2Tran x) " is Relation-like Function-like set
rng ((Mx2Tran x) ") is set
dom (Mx2Tran x) is non empty Element of K19( the carrier of (TOP-REAL m))
[#] (TOP-REAL m) is non empty non proper Element of K19( the carrier of (TOP-REAL m))
((Mx2Tran x) ") " ([#] (Lin (rng (TRn | (len v))))) is set
(Mx2Tran x) .: ([#] (Lin (rng (TRn | (len v))))) is Element of K19( the carrier of (TOP-REAL m))
((Mx2Tran x) ") .: ([#] (Lin M)) is set
x is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
len x is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
TRn | (len x) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
Seg (len x) is finite len x -element V135() V183() V184() V185() V186() V187() V188() Element of K19(NAT)
{ b₁ where b₁ is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b₁ & b₁ <= len x ) } is set
TRn | (Seg (len x)) is Relation-like NAT -defined Seg (len x) -defined NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSubsequence-like set
rng (TRn | (len x)) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Lin (rng (TRn | (len x))) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of m -VectSp_over F_Real
[#] (Lin (rng (TRn | (len x)))) is non empty non proper Element of K19( the carrier of (Lin (rng (TRn | (len x)))))
the carrier of (Lin (rng (TRn | (len x)))) is non empty set
K19( the carrier of (Lin (rng (TRn | (len x))))) is set
L is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
L | (len x) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of F_Real *
L | (Seg (len x)) is Relation-like NAT -defined Seg (len x) -defined NAT -defined the carrier of F_Real * -valued Function-like finite FinSubsequence-like set
Mx2Tran L is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)))
x ~ is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
width (x ~) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
width L is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
F is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of width (x ~),m, the carrier of F_Real
(x ~) * F is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len (x ~), width F, the carrier of F_Real
len (x ~) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
width F is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
F is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
Mx2Tran F is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)))
(Mx2Tran F) .: ([#] (Lin M)) is Element of K19( the carrier of (TOP-REAL m))
((Mx2Tran x) ") (#) (Mx2Tran L) is Relation-like the carrier of (TOP-REAL m) -valued Function-like set
Mx2Tran F is Relation-like the carrier of (TOP-REAL (width (x ~))) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL (width (x ~))), the carrier of (TOP-REAL m)))
TOP-REAL (width (x ~)) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL (width (x ~))) is non empty set
K20( the carrier of (TOP-REAL (width (x ~))), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL (width (x ~))), the carrier of (TOP-REAL m))) is set
((Mx2Tran x) ") (#) (Mx2Tran F) is Relation-like the carrier of (TOP-REAL m) -valued Function-like set
Mx2Tran (x ~) is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)))
(Mx2Tran F) * (Mx2Tran (x ~)) is Relation-like the carrier of (TOP-REAL m) -defined the carrier of (TOP-REAL m) -valued Function-like Element of K19(K20( the carrier of (TOP-REAL m), the carrier of (TOP-REAL m)))
Mx2Tran ((x ~) * F) is Relation-like the carrier of (TOP-REAL (len (x ~))) -defined the carrier of (TOP-REAL (width F)) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL (len (x ~))), the carrier of (TOP-REAL (width F))))
TOP-REAL (len (x ~)) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL (len (x ~))) is non empty set
TOP-REAL (width F) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL (width F)) is non empty set
K20( the carrier of (TOP-REAL (len (x ~))), the carrier of (TOP-REAL (width F))) is Relation-like set
K19(K20( the carrier of (TOP-REAL (len (x ~))), the carrier of (TOP-REAL (width F)))) is set
(Mx2Tran L) .: ([#] (Lin (rng (TRn | (len x))))) is Element of K19( the carrier of (TOP-REAL m))
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
K19( the carrier of (TOP-REAL n)) is set
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
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
Mx2Tran M is Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)))
the carrier of (TOP-REAL m) is non empty set
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m))) is set
MT is affinely-independent linearly-independent Element of K19( the carrier of (TOP-REAL n))
(Mx2Tran M) .: MT is Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is set
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (n -VectSp_over F_Real) is non empty set
1. (F_Real,n) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of F_Real
MX2FinS (1. (F_Real,n)) is Relation-like NAT -defined the carrier of (n -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (n -VectSp_over F_Real)
the carrier of (m -VectSp_over F_Real) is non empty set
1. (F_Real,m) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
MX2FinS (1. (F_Real,m)) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
A is Relation-like NAT -defined the carrier of (n -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of n -VectSp_over F_Real
len A is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
R is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of m -VectSp_over F_Real
len R is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
v is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len A, len R, the carrier of F_Real
Mx2Tran (v,A,R) is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like non empty total quasi_total V157(n -VectSp_over F_Real,m -VectSp_over F_Real) V200( F_Real ,n -VectSp_over F_Real,m -VectSp_over F_Real) Element of K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)))
K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)) is Relation-like set
K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real))) is set
K19( the carrier of (n -VectSp_over F_Real)) is set
x is Element of K19( the carrier of (n -VectSp_over F_Real))
(Mx2Tran (v,A,R)) .: x is Element of K19( the carrier of (m -VectSp_over F_Real))
K19( the carrier of (m -VectSp_over F_Real)) is set
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
R is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of (Mx2Tran (v,A,R)) .: x
Carrier R is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Sum R is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
ker (Mx2Tran (v,A,R)) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n -VectSp_over F_Real
(0). (n -VectSp_over F_Real) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional Subspace of n -VectSp_over F_Real
(Mx2Tran (v,A,R)) | x is Relation-like the carrier of (n -VectSp_over F_Real) -defined x -defined the carrier of (n -VectSp_over F_Real) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like Element of K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)))
(Mx2Tran (v,A,R)) # R is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of x
(Mx2Tran (v,A,R)) @ ((Mx2Tran (v,A,R)) # R) is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
Carrier ((Mx2Tran (v,A,R)) # R) is finite Element of K19( the carrier of (n -VectSp_over F_Real))
(Mx2Tran (v,A,R)) | (Carrier ((Mx2Tran (v,A,R)) # R)) is Relation-like the carrier of (n -VectSp_over F_Real) -defined Carrier ((Mx2Tran (v,A,R)) # R) -defined the carrier of (n -VectSp_over F_Real) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite Element of K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)))
(Mx2Tran (v,A,R)) .: (Carrier ((Mx2Tran (v,A,R)) # R)) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
Sum ((Mx2Tran (v,A,R)) # R) is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
(Mx2Tran (v,A,R)) . (Sum ((Mx2Tran (v,A,R)) # R)) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
0. (n -VectSp_over F_Real) is Relation-like Function-like V64(n -VectSp_over F_Real) Element of the carrier of (n -VectSp_over F_Real)
the ZeroF of (n -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
K19( the carrier of (TOP-REAL n)) is set
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
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
Mx2Tran M is Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)))
the carrier of (TOP-REAL m) is non empty set
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m))) is set
A is affinely-independent Element of K19( the carrier of (TOP-REAL n))
(Mx2Tran M) .: A is Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is set
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like V64( TOP-REAL n) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
{(0. (TOP-REAL n))} is functional non empty V12() finite V38() 1 -element set
R is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- R is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- R is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- R) + A is affinely-independent Element of K19( the carrier of (TOP-REAL n))
((- R) + A) \ {(0. (TOP-REAL n))} is Element of K19( the carrier of (TOP-REAL n))
dom (Mx2Tran M) is non empty Element of K19( the carrier of (TOP-REAL n))
[#] (TOP-REAL n) is non empty non proper Element of K19( the carrier of (TOP-REAL n))
(Mx2Tran M) . R is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(Mx2Tran M) . (0. (TOP-REAL n)) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
{(0. (TOP-REAL m))} is functional non empty V12() finite V38() 1 -element set
Im ((Mx2Tran M),(0. (TOP-REAL n))) is set
(Mx2Tran M) .: {(0. (TOP-REAL n))} is finite Element of K19( the carrier of (TOP-REAL m))
(0. (TOP-REAL n)) - R is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(0. (TOP-REAL n)) - R is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(Mx2Tran M) . (- R) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . R) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . R) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(0. (TOP-REAL m)) - ((Mx2Tran M) . R) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(0. (TOP-REAL m)) - ((Mx2Tran M) . R) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
- ((Mx2Tran M) . R) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
- ((Mx2Tran M) . R) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(Mx2Tran M) .: (((- R) + A) \ {(0. (TOP-REAL n))}) is Element of K19( the carrier of (TOP-REAL m))
(Mx2Tran M) .: ((- R) + A) is Element of K19( the carrier of (TOP-REAL m))
((Mx2Tran M) .: ((- R) + A)) \ ((Mx2Tran M) .: {(0. (TOP-REAL n))}) is Element of K19( the carrier of (TOP-REAL m))
(- ((Mx2Tran M) . R)) + ((Mx2Tran M) .: A) is Element of K19( the carrier of (TOP-REAL m))
((- ((Mx2Tran M) . R)) + ((Mx2Tran M) .: A)) \ {(0. (TOP-REAL m))} is Element of K19( the carrier of (TOP-REAL m))
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL n) is non empty set
K19( the carrier of (TOP-REAL n)) is set
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
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
Mx2Tran M is Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)))
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m))) is set
A is affinely-independent Element of K19( the carrier of (TOP-REAL n))
Affin A is V268( TOP-REAL n) Element of K19( the carrier of (TOP-REAL n))
(Mx2Tran M) .: A is Element of K19( the carrier of (TOP-REAL m))
K19( the carrier of (TOP-REAL m)) is set
Affin ((Mx2Tran M) .: A) is V268( TOP-REAL m) Element of K19( the carrier of (TOP-REAL m))
v is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(Mx2Tran M) . v is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
v |-- A is Relation-like the carrier of (TOP-REAL n) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of A
((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A) is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of (Mx2Tran M) .: A
Carrier (v |-- A) is finite Element of K19( the carrier of (TOP-REAL n))
rng (Mx2Tran M) is non empty Element of K19( the carrier of (TOP-REAL m))
Sum (v |-- A) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
R is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
rng R is finite Element of K19( the carrier of (TOP-REAL n))
(v |-- A) (#) R is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL n)
Sum ((v |-- A) (#) R) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(Mx2Tran M) * R is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
dom (Mx2Tran M) is non empty Element of K19( the carrier of (TOP-REAL n))
[#] (TOP-REAL n) is non empty non proper Element of K19( the carrier of (TOP-REAL n))
L is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
len L is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
len R is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
C is set
F is set
(Mx2Tran M) . F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
F is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(v |-- A) . F is V28() V29() ext-real Element of REAL
F is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran M) . F is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(v |-- A) . F is V28() V29() ext-real set
F is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
F is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran M) . F is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(v |-- A) . F is V28() V29() ext-real set
K20( the carrier of (TOP-REAL m),REAL) is Relation-like non empty V12() non finite complex-valued ext-real-valued real-valued set
K19(K20( the carrier of (TOP-REAL m),REAL)) is non empty V12() non finite set
C is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20( the carrier of (TOP-REAL m),REAL))
Funcs ( the carrier of (TOP-REAL m),REAL) is functional non empty FUNCTION_DOMAIN of the carrier of (TOP-REAL m), REAL
F is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(Mx2Tran M) .: (Carrier (v |-- A)) is finite Element of K19( the carrier of (TOP-REAL m))
F is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of (TOP-REAL m),REAL)
F . F is V28() V29() ext-real Element of REAL
F is set
(Mx2Tran M) . F is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
Fm is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(v |-- A) . Fm is V28() V29() ext-real Element of REAL
F is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of TOP-REAL m
Carrier F is finite Element of K19( the carrier of (TOP-REAL m))
F is set
Fm is set
(Mx2Tran M) . Fm is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
fm is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(v |-- A) . fm is V28() V29() ext-real Element of REAL
vAH is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
F . vAH is V28() V29() ext-real Element of REAL
h is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran M) . h is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(v |-- A) . h is V28() V29() ext-real set
F is set
Fm is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
F . Fm is V28() V29() ext-real Element of REAL
F is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of (Mx2Tran M) .: A
F (#) L is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL m)
K20(NAT, the carrier of (TOP-REAL m)) is Relation-like non empty V12() non finite set
K19(K20(NAT, the carrier of (TOP-REAL m))) is non empty V12() non finite set
Sum (F (#) L) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
len (F (#) L) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
fm is Relation-like NAT -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20(NAT, the carrier of (TOP-REAL m)))
fm . (len (F (#) L)) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
fm . 0 is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
rng L is finite Element of K19( the carrier of (TOP-REAL m))
dom (v |-- A) is Element of K19( the carrier of (TOP-REAL n))
(v |-- A) * R is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len ((v |-- A) * R) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
K20(NAT, the carrier of (TOP-REAL n)) is Relation-like non empty V12() non finite set
K19(K20(NAT, the carrier of (TOP-REAL n))) is non empty V12() non finite set
len ((v |-- A) (#) R) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like V64( TOP-REAL n) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
h is Relation-like NAT -defined the carrier of (TOP-REAL n) -valued Function-like non empty total quasi_total Element of K19(K20(NAT, the carrier of (TOP-REAL n)))
h . (len ((v |-- A) (#) R)) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
h . 0 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
j is V23() V27() V28() V29() finite cardinal ext-real non negative set
fm . j is set
h . j is set
(Mx2Tran M) . (h . j) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
j + 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
fm . (j + 1) is set
h . (j + 1) is set
(Mx2Tran M) . (h . (j + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
J is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
J + 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
f is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of f is non empty set
L /. (J + 1) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
R /. (J + 1) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
Hi is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of Hi is non empty set
dom L is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
MTRj1 is Element of the carrier of f
L . (J + 1) is set
dom R is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
Hj1 is Element of the carrier of Hi
R . (J + 1) is set
(Mx2Tran M) . Hj1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
F . MTRj1 is V28() V29() ext-real set
(v |-- A) . Hj1 is V28() V29() ext-real set
dom ((v |-- A) (#) R) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
((v |-- A) (#) R) . (J + 1) is set
rng ((v |-- A) (#) R) is finite Element of K19( the carrier of (TOP-REAL n))
dom (F (#) L) is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
(F (#) L) . (J + 1) is set
rng (F (#) L) is finite Element of K19( the carrier of (TOP-REAL m))
vAHj1 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(Mx2Tran M) . vAHj1 is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
((v |-- A) . Hj1) * Hj1 is Element of the carrier of Hi
(Mx2Tran M) . (((v |-- A) . Hj1) * Hj1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
hj1 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
((v |-- A) . Hj1) * hj1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(Mx2Tran M) . (((v |-- A) . Hj1) * hj1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran M) . hj1 is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
((v |-- A) . Hj1) * ((Mx2Tran M) . hj1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(F . MTRj1) * MTRj1 is Element of the carrier of f
Fmj1 is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
h . (J + 1) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
h . J is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(h . J) + vAHj1 is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(h . J) + vAHj1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
h . (j + 1) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(Mx2Tran M) . (h . (j + 1)) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(Mx2Tran M) . (h . J) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
((Mx2Tran M) . (h . J)) + ((Mx2Tran M) . vAHj1) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
((Mx2Tran M) . (h . J)) + ((Mx2Tran M) . vAHj1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
fm . (j + 1) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
fm . 0 is set
h . 0 is set
(Mx2Tran M) . (h . 0) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran M) . (Sum ((v |-- A) (#) R)) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
Sum F is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
f is V23() V27() V28() V29() finite cardinal ext-real non negative set
dom R is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
((v |-- A) * R) . f is V28() V29() ext-real set
R . f is set
(v |-- A) . (R . f) is V28() V29() ext-real set
L . f is set
(Mx2Tran M) . (R . f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
dom L is finite V183() V184() V185() V186() V187() V188() Element of K19(NAT)
F * L is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(F * L) . f is V28() V29() ext-real set
F . (L . f) is V28() V29() ext-real set
Hi is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(Mx2Tran M) . Hi is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
j is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(Mx2Tran M) . j is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(v |-- A) . j is V28() V29() ext-real set
dom F is Element of K19( the carrier of (TOP-REAL m))
[#] (TOP-REAL m) is non empty non proper Element of K19( the carrier of (TOP-REAL m))
len (F * L) is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
Sum (F * L) is V28() V29() ext-real Element of REAL
sum (v |-- A) is V28() V29() ext-real Element of REAL
sum F is V28() V29() ext-real Element of REAL
{ (Sum b₁) where b₁ is Relation-like the carrier of (TOP-REAL m) -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Linear_Combination of (Mx2Tran M) .: A : sum b₁ = 1 } is set
f is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(v |-- A) . f is V28() V29() ext-real set
(Mx2Tran M) . f is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
(((Mx2Tran M) . v) |-- ((Mx2Tran M) .: A)) . ((Mx2Tran M) . f) is V28() V29() ext-real set
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K19( the carrier of (TOP-REAL m)) is set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
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
Mx2Tran M is Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)))
the carrier of (TOP-REAL n) is non empty set
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m))) is set
MT is affinely-independent linearly-independent Element of K19( the carrier of (TOP-REAL m))
(Mx2Tran M) " MT is Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is set
n -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
m -VectSp_over F_Real is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional VectSpStr over F_Real
the carrier of (m -VectSp_over F_Real) is non empty set
1. (F_Real,m) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of m,m, the carrier of F_Real
MX2FinS (1. (F_Real,m)) is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (m -VectSp_over F_Real)
K19( the carrier of (m -VectSp_over F_Real)) is set
the carrier of (n -VectSp_over F_Real) is non empty set
1. (F_Real,n) is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of F_Real
MX2FinS (1. (F_Real,n)) is Relation-like NAT -defined the carrier of (n -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (n -VectSp_over F_Real)
v is Relation-like NAT -defined the carrier of (n -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of n -VectSp_over F_Real
len v is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
A is Relation-like NAT -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of m -VectSp_over F_Real
len A is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT
x is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of len v, len A, the carrier of F_Real
Mx2Tran (x,v,A) is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like non empty total quasi_total V157(n -VectSp_over F_Real,m -VectSp_over F_Real) V200( F_Real ,n -VectSp_over F_Real,m -VectSp_over F_Real) Element of K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)))
K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)) is Relation-like set
K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real))) is set
rng (Mx2Tran (x,v,A)) is non empty Element of K19( the carrier of (m -VectSp_over F_Real))
MT /\ (rng (Mx2Tran (x,v,A))) is Element of K19( the carrier of (m -VectSp_over F_Real))
R is Element of K19( the carrier of (m -VectSp_over F_Real))
R is Element of K19( the carrier of (m -VectSp_over F_Real))
dom (Mx2Tran (x,v,A)) is non empty Element of K19( the carrier of (n -VectSp_over F_Real))
K19( the carrier of (n -VectSp_over F_Real)) is set
[#] (n -VectSp_over F_Real) is non empty non proper Element of K19( the carrier of (n -VectSp_over F_Real))
(Mx2Tran (x,v,A)) " R is Element of K19( the carrier of (n -VectSp_over F_Real))
0. (n -VectSp_over F_Real) is Relation-like Function-like V64(n -VectSp_over F_Real) Element of the carrier of (n -VectSp_over F_Real)
the ZeroF of (n -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
L is Relation-like the carrier of (n -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of (Mx2Tran (x,v,A)) " R
Carrier L is finite Element of K19( the carrier of (n -VectSp_over F_Real))
Sum L is Relation-like Function-like Element of the carrier of (n -VectSp_over F_Real)
(Mx2Tran (x,v,A)) .: ((Mx2Tran (x,v,A)) " R) is Element of K19( the carrier of (m -VectSp_over F_Real))
(Mx2Tran (x,v,A)) @ L is Relation-like the carrier of (m -VectSp_over F_Real) -defined the carrier of F_Real -valued Function-like total quasi_total Linear_Combination of m -VectSp_over F_Real
(Mx2Tran (x,v,A)) .: (Carrier L) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
(Mx2Tran (x,v,A)) | (Carrier L) is Relation-like the carrier of (n -VectSp_over F_Real) -defined Carrier L -defined the carrier of (n -VectSp_over F_Real) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like finite Element of K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)))
Carrier ((Mx2Tran (x,v,A)) @ L) is finite Element of K19( the carrier of (m -VectSp_over F_Real))
(Mx2Tran (x,v,A)) | ((Mx2Tran (x,v,A)) " R) is Relation-like the carrier of (n -VectSp_over F_Real) -defined (Mx2Tran (x,v,A)) " R -defined the carrier of (n -VectSp_over F_Real) -defined the carrier of (m -VectSp_over F_Real) -valued Function-like Element of K19(K20( the carrier of (n -VectSp_over F_Real), the carrier of (m -VectSp_over F_Real)))
Sum ((Mx2Tran (x,v,A)) @ L) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
(Mx2Tran (x,v,A)) . (Sum L) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
0. (m -VectSp_over F_Real) is Relation-like Function-like V64(m -VectSp_over F_Real) Element of the carrier of (m -VectSp_over F_Real)
the ZeroF of (m -VectSp_over F_Real) is Relation-like Function-like Element of the carrier of (m -VectSp_over F_Real)
(Mx2Tran (x,v,A)) " MT is Element of K19( the carrier of (n -VectSp_over F_Real))
m is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL m is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
the carrier of (TOP-REAL m) is non empty set
K19( the carrier of (TOP-REAL m)) is set
n is V23() V27() V28() V29() finite cardinal ext-real non negative set
TOP-REAL n is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() L18()
M is Relation-like NAT -defined the carrier of F_Real * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,m, the carrier of F_Real
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
Mx2Tran M is Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL m) -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)))
the carrier of (TOP-REAL n) is non empty set
K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m)) is Relation-like set
K19(K20( the carrier of (TOP-REAL n), the carrier of (TOP-REAL m))) is set
A is affinely-independent Element of K19( the carrier of (TOP-REAL m))
(Mx2Tran M) " A is Element of K19( the carrier of (TOP-REAL n))
K19( the carrier of (TOP-REAL n)) is set
rng (Mx2Tran M) is non empty Element of K19( the carrier of (TOP-REAL m))
A /\ (rng (Mx2Tran M)) is Element of K19( the carrier of (TOP-REAL m))
(Mx2Tran M) " (A /\ (rng (Mx2Tran M))) is Element of K19( the carrier of (TOP-REAL n))
R is affinely-independent Element of K19( the carrier of (TOP-REAL m))
R is affinely-independent Element of K19( the carrier of (TOP-REAL m))
0. (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like V64( TOP-REAL m) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
the ZeroF of (TOP-REAL m) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
{(0. (TOP-REAL m))} is functional non empty V12() finite V38() 1 -element set
v is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
- v is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
- v is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(- v) + R is affinely-independent Element of K19( the carrier of (TOP-REAL m))
((- v) + R) \ {(0. (TOP-REAL m))} is Element of K19( the carrier of (TOP-REAL m))
dom (Mx2Tran M) is non empty Element of K19( the carrier of (TOP-REAL n))
x is set
(Mx2Tran M) . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued set
x is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- x is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
- x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
0. (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like V64( TOP-REAL n) complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
the ZeroF of (TOP-REAL n) is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(0. (TOP-REAL n)) - x is Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL n)
(0. (TOP-REAL n)) - x is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(Mx2Tran M) . (- x) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(Mx2Tran M) . (0. (TOP-REAL n)) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(Mx2Tran M) . x is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . x) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . x) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
(0. (TOP-REAL m)) - ((Mx2Tran M) . x) is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of the carrier of (TOP-REAL m)
(0. (TOP-REAL m)) - ((Mx2Tran M) . x) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
[#] (TOP-REAL n) is non empty non proper Element of K19( the carrier of (TOP-REAL n))
Im ((Mx2Tran M),(0. (TOP-REAL n))) is set
{(0. (TOP-REAL n))} is functional non empty V12() finite V38() 1 -element set
(Mx2Tran M) .: {(0. (TOP-REAL n))} is finite Element of K19( the carrier of (TOP-REAL m))
(Mx2Tran M) " {(0. (TOP-REAL m))} is Element of K19( the carrier of (TOP-REAL n))
(Mx2Tran M) " (((- v) + R) \ {(0. (TOP-REAL m))}) is Element of K19( the carrier of (TOP-REAL n))
(Mx2Tran M) " ((- v) + R) is Element of K19( the carrier of (TOP-REAL n))
((Mx2Tran M) " ((- v) + R)) \ {(0. (TOP-REAL n))} is Element of K19( the carrier of (TOP-REAL n))
(Mx2Tran M) " R is Element of K19( the carrier of (TOP-REAL n))
(- x) + ((Mx2Tran M) " R) is Element of K19( the carrier of (TOP-REAL n))
((- x) + ((Mx2Tran M) " R)) \ {(0. (TOP-REAL n))} is Element of K19( the carrier of (TOP-REAL n))
R is affinely-independent Element of K19( the carrier of (TOP-REAL m))