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)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
the carrier of F_Real * is functional non empty FinSequence-membered FinSequenceSet of the carrier of F_Real
0. F_Real is V28() V29() V64( F_Real ) ext-real Element of the carrier of F_Real
the ZeroF of F_Real is V28() V29() ext-real Element of the carrier of F_Real
<*> 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)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
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)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(Line (MT,x)) . F is set
F is V23() V27() V28() V29() finite cardinal ext-real non negative set
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)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
K19((Seg n)) is finite V38() set
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)
{ b1 where b1 is V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() Element of NAT : ( 1 <= b1 & b1 <= TRm ) } is set
K19((Seg TRm)) is finite V38() set
A is V23() V27() V28() V29() finite cardinal ext-real non negative set
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