begin
definition
let R be ( ( non
empty right_complementable V94()
well-unital V102()
Abelian add-associative right_zeroed ) ( non
empty right_complementable V92()
V94()
right-distributive left-distributive right_unital well-unital V102()
left_unital Abelian add-associative right_zeroed )
Ring) ;
let V be ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
R : ( ( non
empty right_complementable V94()
well-unital V102()
Abelian add-associative right_zeroed ) ( non
empty right_complementable V92()
V94()
right-distributive left-distributive right_unital well-unital V102()
left_unital Abelian add-associative right_zeroed )
Ring) ) ;
let A be ( ( ) ( )
Subset of ) ;
func Lin A -> ( (
strict ) ( non
empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
Subspace of
V : ( ( ) ( )
1-sorted ) )
means
the
carrier of
it : ( (
Function-like quasi_total ) (
Relation-like [:A : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,A : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( )
set )
-defined A : ( ( ) ( )
BiModStr over
R : ( ( ) ( )
1-sorted ) ,
V : ( ( ) ( )
1-sorted ) )
-valued Function-like quasi_total )
Element of
bool [:[:A : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ,A : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( ) set ) ,A : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= { (Sum l : ( ( ) ( Relation-like the carrier of V : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) LeftMod of R : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) -defined the carrier of R : ( ( non empty right_complementable V94() well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable V92() V94() right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) Subset of ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) where l is ( ( ) ( Relation-like the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Linear_Combination of A : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) : verum } ;
end;
definition
let R be ( ( non
empty right_complementable V94()
well-unital V102()
Abelian add-associative right_zeroed ) ( non
empty right_complementable V92()
V94()
right-distributive left-distributive right_unital well-unital V102()
left_unital Abelian add-associative right_zeroed )
Ring) ;
let V be ( ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ) ( non
empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
LeftMod of
R : ( ( non
empty right_complementable V94()
well-unital V102()
Abelian add-associative right_zeroed ) ( non
empty right_complementable V92()
V94()
right-distributive left-distributive right_unital well-unital V102()
left_unital Abelian add-associative right_zeroed )
Ring) ) ;
let IT be ( ( ) ( )
Subset of ) ;
attr IT is
base means
(
IT : ( ( ) ( )
BiModStr over
R : ( ( ) ( )
1-sorted ) ,
V : ( ( ) ( )
1-sorted ) ) is
linearly-independent &
Lin IT : ( ( ) ( )
BiModStr over
R : ( ( ) ( )
1-sorted ) ,
V : ( ( ) ( )
1-sorted ) ) : ( (
strict ) ( non
empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed )
Subspace of
V : ( ( ) ( )
1-sorted ) )
= VectSpStr(# the
carrier of
V : ( ( ) ( )
1-sorted ) : ( ( ) ( )
set ) , the
addF of
V : ( ( ) ( )
1-sorted ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( ( ) ( )
1-sorted ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) , the
ZeroF of
V : ( ( ) ( )
1-sorted ) : ( ( ) ( )
Element of the
carrier of
V : ( ( ) ( )
1-sorted ) : ( ( ) ( )
set ) ) , the
lmult of
V : ( ( ) ( )
1-sorted ) : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set )
-defined the
carrier of
V : ( ( ) ( )
1-sorted ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Element of
bool [:[: the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) #) : ( (
strict ) (
strict )
VectSpStr over
R : ( ( ) ( )
1-sorted ) ) );
end;