begin
begin
theorem
for
m,
n being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
for
M being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
m : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) st
the_rank_of M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
V23()
V27()
V28()
V29()
V30()
V31()
finite cardinal ext-real non
negative V183()
V184()
V185()
V186()
V187()
V188() )
Element of
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) )
= n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) holds
M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) is ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
(Lin (lines b3 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of (b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional ) VectSpStr over F_Real : ( ( strict ) ( 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 ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) : ( ( ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
OrdBasis of
Lin (lines M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) ) ;
theorem
for
K being ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field)
for
V,
W being ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
K : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) )
for
T being ( (
Function-like quasi_total V157(
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
V200(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ) ) (
Relation-like the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V157(
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
V200(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ) )
linear-transformation of
V : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
W : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
for
A being ( ( ) ( )
Subset of )
for
L being ( ( ) (
Relation-like the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) : ( ( ) ( non
empty V12() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
A : ( ( ) ( )
Subset of ) ) st
T : ( (
Function-like quasi_total V157(
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
V200(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ) ) (
Relation-like the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V157(
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
V200(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ) )
linear-transformation of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
| A : ( ( ) ( )
Subset of ) : ( (
Function-like ) (
Relation-like b5 : ( ( ) ( )
Subset of )
-defined the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
K19(
K20( the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set ) , the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) ) is
one-to-one holds
T : ( (
Function-like quasi_total V157(
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
V200(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ) ) (
Relation-like the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total V157(
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
V200(
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ,
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ) )
linear-transformation of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ,
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) )
. (Sum L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) : ( ( ) ( non empty V12() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b5 : ( ( ) ( ) Subset of ) ) ) : ( ( ) ( )
Element of the
carrier of
b2 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set ) )
= Sum (T : ( ( Function-like quasi_total V157(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ,b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ) V200(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ,b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ) ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total V157(b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ,b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ) V200(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ,b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ,b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ) ) linear-transformation of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ,b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) ) @ L : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) VectSp of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141() V143() well-unital V149() ) ( 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 ) Field) : ( ( ) ( non empty V12() ) set ) -valued Function-like total quasi_total ) Linear_Combination of b5 : ( ( ) ( ) Subset of ) ) ) : ( ( ) (
Relation-like the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) : ( ( ) ( non
empty V12() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) ) : ( ( ) ( )
Element of the
carrier of
b3 : ( ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital )
VectSp of
b1 : ( ( non
empty non
degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed V141()
V143()
well-unital V149() ) ( 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 )
Field) ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
m,
n being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
for
f being ( (
Relation-like Function-like b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence)
for
M being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
m : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
for
S being ( ( ) (
finite V183()
V184()
V185()
V186()
V187()
V188() )
Subset of ( ( ) (
finite V38() )
set ) ) st
M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
| S : ( ( ) (
finite V183()
V184()
V185()
V186()
V187()
V188() )
Subset of ( ( ) (
finite V38() )
set ) ) : ( (
Function-like ) (
Relation-like b5 : ( ( ) (
finite V183()
V184()
V185()
V186()
V187()
V188() )
Subset of ( ( ) (
finite V38() )
set ) )
-defined NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSubsequence-like )
Element of
K19(
K20(
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) ,
( the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) *) : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) ) : ( ( ) (
Relation-like non
empty V12() non
finite )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) is
one-to-one &
rng (M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) | S : ( ( ) ( finite V183() V184() V185() V186() V187() V188() ) Subset of ( ( ) ( finite V38() ) set ) ) ) : ( (
Function-like ) (
Relation-like b5 : ( ( ) (
finite V183()
V184()
V185()
V186()
V187()
V188() )
Subset of ( ( ) (
finite V38() )
set ) )
-defined NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSubsequence-like )
Element of
K19(
K20(
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) ,
( the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) *) : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) ) : ( ( ) (
Relation-like non
empty V12() non
finite )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) : ( ( ) (
functional finite FinSequence-membered )
Element of
K19(
( the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) *) : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) ) : ( ( ) ( )
set ) )
= lines M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) holds
ex
L being ( ( ) (
Relation-like the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
lines M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ) st
(
Sum L : ( ( ) (
Relation-like the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
lines b4 : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like )
Element of the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) )
= (Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
K19(
K20( the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) )
. f : ( (
Relation-like Function-like b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
set ) & ( for
k being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) st
k : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
in S : ( ( ) (
finite V183()
V184()
V185()
V186()
V187()
V188() )
Subset of ( ( ) (
finite V38() )
set ) ) holds
L : ( ( ) (
Relation-like the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
lines b4 : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) )
. (Line (M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ,k : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) )) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like finite width b4 : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
V23()
V27()
V28()
V29()
V30()
V31()
finite cardinal ext-real non
negative V183()
V184()
V185()
V186()
V187()
V188() )
Element of
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) )
-element FinSequence-like FinSubsequence-like )
Element of
(width b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) (
V23()
V27()
V28()
V29()
V30()
V31()
finite cardinal ext-real non
negative V183()
V184()
V185()
V186()
V187()
V188() )
Element of
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) )
-tuples_on the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) ) : ( ( ) ( )
set )
= Sum (Seq (f : ( ( Relation-like Function-like b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -element FinSequence-like real-valued ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined Function-like finite b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) | (M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) " {(Line (M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ,k : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) -valued Function-like finite width b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) : ( ( ) ( V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() ) Element of NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) -element FinSequence-like FinSubsequence-like ) Element of (width b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() ) Element of NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) -tuples_on the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) } : ( ( ) ( functional non empty V12() finite V38() 1 : ( ( ) ( non empty V23() V27() V28() V29() V30() V31() finite cardinal ext-real positive non negative V183() V184() V185() V186() V187() V188() ) Element of NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) -element ) set ) ) : ( ( ) ( finite V183() V184() V185() V186() V187() V188() ) Element of K19(NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) : ( ( Relation-like ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) " {(Line (b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ,b7 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) -valued Function-like finite width b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) : ( ( ) ( V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() ) Element of NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) -element FinSequence-like FinSubsequence-like ) Element of (width b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( V23() V27() V28() V29() V30() V31() finite cardinal ext-real non negative V183() V184() V185() V186() V187() V188() ) Element of NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) -tuples_on the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) } : ( ( ) ( functional non empty V12() finite V38() 1 : ( ( ) ( non empty V23() V27() V28() V29() V30() V31() finite cardinal ext-real positive non negative V183() V184() V185() V186() V187() V188() ) Element of NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) -element ) set ) : ( ( ) ( finite V183() V184() V185() V186() V187() V188() ) Element of K19(NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined Function-like finite FinSubsequence-like complex-valued ext-real-valued real-valued ) set ) ) : ( (
Relation-like Function-like ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
set ) : ( (
V28() ) (
V28()
V29()
ext-real )
set ) ) ) ;
theorem
for
n,
m being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
for
f being ( (
Relation-like Function-like b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence)
for
M being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
m : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) st
M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) is
without_repeated_line holds
ex
L being ( ( ) (
Relation-like the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
lines M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ) st
(
Sum L : ( ( ) (
Relation-like the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
lines b4 : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like )
Element of the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) )
= (Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
K19(
K20( the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) )
. f : ( (
Relation-like Function-like b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
set ) & ( for
k being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) st
k : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
in dom f : ( (
Relation-like Function-like b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence) : ( ( ) (
finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element V183()
V184()
V185()
V186()
V187()
V188() )
Element of
K19(
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) holds
L : ( ( ) (
Relation-like the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like total quasi_total )
Linear_Combination of
lines b4 : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) )
. (Line (M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ,k : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) )) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like finite width b4 : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
V23()
V27()
V28()
V29()
V30()
V31()
finite cardinal ext-real non
negative V183()
V184()
V185()
V186()
V187()
V188() )
Element of
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) )
-element FinSequence-like FinSubsequence-like )
Element of
(width b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) (
V23()
V27()
V28()
V29()
V30()
V31()
finite cardinal ext-real non
negative V183()
V184()
V185()
V186()
V187()
V188() )
Element of
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) )
-tuples_on the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) ) : ( ( ) ( )
set )
= f : ( (
Relation-like Function-like b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence)
. k : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) : ( ( ) (
V28()
V29()
ext-real )
set ) ) ) ;
theorem
for
n,
m being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
for
f being ( (
Relation-like Function-like b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence)
for
M being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
m : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
for
B being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
(Lin (lines b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of (b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional ) VectSpStr over F_Real : ( ( strict ) ( 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 ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) : ( ( ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
OrdBasis of
Lin (lines M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) ) st
B : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
(Lin (lines b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of (b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional ) VectSpStr over F_Real : ( ( strict ) ( 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 ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) : ( ( ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
OrdBasis of
Lin (lines b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) )
= M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) holds
for
Mf being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
Mf : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
= (Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
K19(
K20( the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) )
. f : ( (
Relation-like Function-like b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
set ) holds
Mf : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
|-- B : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
(Lin (lines b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of (b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional ) VectSpStr over F_Real : ( ( strict ) ( 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 ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) : ( ( ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
OrdBasis of
Lin (lines b4 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) (
finite )
Element of
K19( the
carrier of
(b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) ) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
= f : ( (
Relation-like Function-like b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence) ;
theorem
for
n,
m being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
for
M being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
m : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) holds
rng (Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
K19(
K20( the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
K19( the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
= [#] (Lin (lines M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of (b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional ) VectSpStr over F_Real : ( ( strict ) ( 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 ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) : ( ( ) ( non
empty non
proper )
Element of
K19( the
carrier of
(Lin (lines b3 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( ) ( finite ) Element of K19( the carrier of (b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -VectSp_over F_Real : ( ( strict ) ( 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 ) ) : ( ( strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional ) VectSpStr over F_Real : ( ( strict ) ( 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 ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
Subspace of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-VectSp_over F_Real : ( (
strict ) ( 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 ) : ( (
strict ) ( non
empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital finite-dimensional )
VectSpStr over
F_Real : ( (
strict ) ( 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 ) ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ;
begin
theorem
for
m,
n being ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
for
M being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
m : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
for
A being ( (
affinely-independent ) (
affinely-independent )
Subset of ) st
the_rank_of M : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set )
* : ( ( ) (
functional non
empty FinSequence-membered )
FinSequenceSet of the
carrier of
F_Real : ( (
strict ) ( 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 ) : ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) )
-valued Function-like finite FinSequence-like FinSubsequence-like tabular )
Matrix of
b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) ,
b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) , ( ( ) ( non
empty V12()
V183()
V184()
V185() )
set ) ) : ( ( ) (
V23()
V27()
V28()
V29()
V30()
V31()
finite cardinal ext-real non
negative V183()
V184()
V185()
V186()
V187()
V188() )
Element of
NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) ) )
= n : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) holds
for
v being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
Element of ( ( ) ( non
empty )
set ) ) st
v : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
Element of ( ( ) ( non
empty )
set ) )
in Affin A : ( (
affinely-independent ) (
affinely-independent )
Subset of ) : ( ( ) (
V268(
TOP-REAL b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) ) )
Element of
K19( the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) holds
(
(Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
K19(
K20( the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) )
. v : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
Element of the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) )
in Affin ((Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) .: A : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( )
Element of
K19( the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V268(
TOP-REAL b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) ) )
Element of
K19( the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) & ( for
f being ( (
Relation-like Function-like b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence) holds
(v : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined Function-like finite b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of ( ( ) ( non empty ) set ) ) |-- A : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) (
Relation-like the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set )
-valued Function-like total quasi_total complex-valued ext-real-valued real-valued )
Linear_Combination of
b4 : ( (
affinely-independent ) (
affinely-independent )
Subset of ) )
. f : ( (
Relation-like Function-like b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like real-valued ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b2 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
FinSequence) : ( ( ) (
V28()
V29()
ext-real )
set )
= (((Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . v : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined Function-like finite b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined Function-like finite b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) ) |-- ((Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) .: A : ( ( affinely-independent ) ( affinely-independent ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
Relation-like the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set )
-valued Function-like total quasi_total complex-valued ext-real-valued real-valued )
Linear_Combination of
(Mx2Tran b3 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
K19(
K20( the
carrier of
(TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
Relation-like )
set ) ) : ( ( ) ( )
set ) )
.: b4 : ( (
affinely-independent ) (
affinely-independent )
Subset of ) : ( ( ) ( )
Element of
K19( the
carrier of
(TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( (
V231() ) ( non
empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231()
V237()
V238() )
L18()) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) )
. ((Mx2Tran M : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of F_Real : ( ( strict ) ( 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 ) : ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) -valued Function-like finite FinSequence-like FinSubsequence-like tabular ) Matrix of b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ,b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) , ( ( ) ( non empty V12() V183() V184() V185() ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -defined the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of (TOP-REAL b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL b1 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) ) : ( ( V231() ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital TopSpace-like V231() V237() V238() ) L18()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . f : ( ( Relation-like Function-like b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -element FinSequence-like real-valued ) ( Relation-like NAT : ( ( ) ( non empty V12() V23() non finite cardinal limit_cardinal V183() V184() V185() V186() V187() V188() V189() ) Element of K19(REAL : ( ( ) ( non empty V12() non finite V183() V184() V185() V189() ) set ) ) : ( ( ) ( non empty V12() non finite ) set ) ) -defined Function-like finite b2 : ( ( V27() ) ( V23() V27() V28() V29() finite cardinal ext-real non negative ) Nat) -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ) : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty V12()
V23() non
finite cardinal limit_cardinal V183()
V184()
V185()
V186()
V187()
V188()
V189() )
Element of
K19(
REAL : ( ( ) ( non
empty V12() non
finite V183()
V184()
V185()
V189() )
set ) ) : ( ( ) ( non
empty V12() non
finite )
set ) )
-defined Function-like finite b1 : ( (
V27() ) (
V23()
V27()
V28()
V29()
finite cardinal ext-real non
negative )
Nat)
-element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued )
set ) : ( ( ) (
V28()
V29()
ext-real )
set ) ) ) ;