:: 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

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

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

(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

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

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