begin
definition
let R be ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) ;
let V be ( ( non
empty right_complementable V105(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V106(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V107(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V108(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V112()
V113()
V114() ) ( non
empty right_complementable V105(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V106(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V107(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V108(
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) )
V112()
V113()
V114() )
LeftMod of
R : ( ( non
empty non
degenerated right_complementable V94()
V96()
well-unital V102()
V112()
V113()
V114()
domRing-like ) ( non
empty non
degenerated V47()
right_complementable V92()
V94()
V96()
right-distributive left-distributive right_unital well-unital V102()
left_unital V112()
V113()
V114()
domRing-like )
domRing) ) ;
let A be ( ( ) ( )
Subset of ) ;
func Lin A -> ( (
strict ) ( non
empty right_complementable strict V105(
R : ( ( ) ( )
1-sorted ) )
V106(
R : ( ( ) ( )
1-sorted ) )
V107(
R : ( ( ) ( )
1-sorted ) )
V108(
R : ( ( ) ( )
1-sorted ) )
V112()
V113()
V114() )
Subspace of
V : ( ( ) ( )
1-sorted ) )
means
the
carrier of
it : ( (
Function-like quasi_total ) (
Relation-like K20(
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
K19(
K20(
K20(
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 V105(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V106(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V107(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V108(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V112() V113() V114() ) ( non empty right_complementable V105(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V106(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V107(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V108(R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) V112() V113() V114() ) LeftMod of R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) ) : ( ( ) ( non empty ) set ) -defined the carrier of R : ( ( non empty non degenerated right_complementable V94() V96() well-unital V102() V112() V113() V114() domRing-like ) ( non empty non degenerated V47() right_complementable V92() V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V112() V113() V114() domRing-like ) domRing) : ( ( ) ( non empty V12() ) 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;