attr V1 is linearly-closed means :: RMOD_2:def 1
( ( for v, u being ( ( ) ( right_complementable ) Vector of ( ( ) ( ) set ) ) st v : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) & u : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) holds
v : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in V1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) & ( for a being ( ( ) ( right_complementable ) Scalar of ( ( ) ( ) set ) )
for v being ( ( ) ( right_complementable ) Vector of ( ( ) ( ) set ) ) st v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) in V1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) holds
v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) * a : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) in V1 : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) );

mode Submodule of V -> ( ( non empty right_complementable Abelian add-associative right_zeroed RightMod-like ) ( non empty right_complementable Abelian add-associative right_zeroed RightMod-like ) RightMod of R : ( ( ) ( ) 1-sorted ) ) means :: RMOD_2:def 2
( the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) c= the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) & 0. it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( V49(it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) ) ) Element of the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) = 0. V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) & the addF of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the addF of V : ( ( ) ( ) 1-sorted ) : ( ( Function-like V18([: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) | [: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) & the rmult of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( Function-like V18([: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the rmult of V : ( ( ) ( ) 1-sorted ) : ( ( Function-like V18([: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like Function-like V18([: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) | [: the carrier of it : ( ( ) ( ) BiModStr over R : ( ( ) ( ) 1-sorted ) ,V : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) );

cluster non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like for ( ( ) ( ) Submodule of V : ( ( non empty right_complementable Abelian add-associative right_zeroed RightMod-like ) ( non empty right_complementable Abelian add-associative right_zeroed RightMod-like ) RightModStr over R : ( ( non empty right_complementable associative well-unital V102() Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ;