:: VECTSP_2 semantic presentation

begin

registration
cluster non empty right_complementable strict unital distributive Abelian add-associative right_zeroed for ( ( ) ( ) doubleLoopStr ) ;
end;

definition
let IT be ( ( non empty ) ( non empty ) multLoopStr_0 ) ;
attr IT is domRing-like means :: VECTSP_2:def 1
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) = 0. IT : ( ( ) ( ) AlgebraStr ) : ( ( ) ( V46(IT : ( ( ) ( ) AlgebraStr ) ) ) Element of the carrier of IT : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) or x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. IT : ( ( ) ( ) AlgebraStr ) : ( ( ) ( V46(IT : ( ( ) ( ) AlgebraStr ) ) ) Element of the carrier of IT : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) or y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = 0. IT : ( ( ) ( ) AlgebraStr ) : ( ( ) ( V46(IT : ( ( ) ( ) AlgebraStr ) ) ) Element of the carrier of IT : ( ( ) ( ) AlgebraStr ) : ( ( ) ( ) set ) ) );
end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible strict unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like for ( ( ) ( ) doubleLoopStr ) ;
end;

definition
mode comRing is ( ( non empty right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
end;

definition
mode domRing is ( ( non empty non degenerated right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like ) ( non empty non degenerated non trivial right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like ) comRing) ;
end;

theorem :: VECTSP_2:1
for F being ( ( non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Field) holds F : ( ( non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Field) is ( ( non empty non degenerated right_complementable associative commutative well-unital distributive Abelian add-associative right_zeroed domRing-like ) ( non empty non degenerated non trivial right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed domRing-like ) domRing) ;

definition
mode Skew-Field is ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
end;

registration
cluster non empty commutative left_unital -> non empty well-unital for ( ( ) ( ) multLoopStr ) ;
cluster non empty commutative right_unital -> non empty well-unital for ( ( ) ( ) multLoopStr ) ;
end;

theorem :: VECTSP_2:2
for R being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr )
for x, y, z being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) holds
( ( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) implies x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) implies x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) & ( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) implies y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) & ( y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) implies x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: VECTSP_2:3
for R being ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr )
for x being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = 0. R : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) iff - x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) = 0. R : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed ) ( non empty right_complementable add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: VECTSP_2:4
for R being ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr )
for x, y being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) ex z being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) + z : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) & x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = z : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: VECTSP_2:5
for F being ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr )
for x, y being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) = 1. F : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) <> 0. F : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) <> 0. F : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable right-distributive left-distributive distributive add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:6
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr )
for x being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) holds
ex y being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) = 1. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:7
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr )
for x, y being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) st y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) = 1. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) = 1. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:8
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr )
for x, y, z being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) * z : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) holds
y : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) = z : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) ;

definition
let SF be ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) ;
let x be ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) ;
assume x : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( V46(SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty non trivial ) set ) ) ;
redefine func x " means :: VECTSP_2:def 2
it : ( ( V6() V18([:SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V6() V18([:SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) Element of bool [:[:SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * x : ( ( ) ( ) VectSpStr over SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( right_complementable ) Element of the carrier of SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) = 1. SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( right_complementable ) Element of the carrier of SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let SF be ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ;
let x, y be ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ;
func x / y -> ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) equals :: VECTSP_2:def 3
x : ( ( ) ( ) VectSpStr over SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) * (y : ( ( V6() V18([:SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ( V6() V18([:SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) Element of bool [:[:SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) ,SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of SF : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: VECTSP_2:9
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = 1. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) & (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = 1. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:10
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for y, x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = 1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) " : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) " : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:11
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x, y being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) & y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
(x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) * (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) " : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:12
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x, y being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) holds
( not x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) or x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) or y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:13
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) " : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:14
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
(x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) " : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:15
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
( (1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) " : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) & (1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:16
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * ((1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = 1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) & ((1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = 1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:17
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = 1_ SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:18
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for y, z, x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:19
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for y, x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
( - (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = (- x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) & x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / (- y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = - (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:20
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for z, x, y being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
( (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) + (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) & (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) - (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) - y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) ;

theorem :: VECTSP_2:21
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for y, z, x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) & z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * z : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) / y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ;

theorem :: VECTSP_2:22
for SF being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field)
for y, x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) st y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. SF : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) holds
(x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) / y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Skew-Field) : ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ;

definition
let FS be ( ( ) ( ) 1-sorted ) ;
attr c2 is strict ;
struct RightModStr over FS -> ( ( ) ( ) addLoopStr ) ;
aggr RightModStr(# carrier, addF, ZeroF, rmult #) -> ( ( strict ) ( strict ) RightModStr over FS : ( ( ) ( ) 1-sorted ) ) ;
sel rmult c2 -> ( ( V6() V18([: the carrier of c2 : ( ( ) ( ) VectSpStr over FS : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of c2 : ( ( ) ( ) VectSpStr over FS : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) ( V6() V18([: the carrier of c2 : ( ( ) ( ) VectSpStr over FS : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of c2 : ( ( ) ( ) VectSpStr over FS : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Function of [: the carrier of c2 : ( ( ) ( ) VectSpStr over FS : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of c2 : ( ( ) ( ) VectSpStr over FS : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let FS be ( ( ) ( ) 1-sorted ) ;
cluster non empty for ( ( ) ( ) RightModStr over FS : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let FS be ( ( ) ( ) 1-sorted ) ;
let A be ( ( non empty ) ( non empty ) set ) ;
let a be ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) BinOp of A : ( ( non empty ) ( non empty ) set ) ) ;
let Z be ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ;
let r be ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Function of [:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ;
cluster RightModStr(# A : ( ( non empty ) ( non empty ) set ) ,a : ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,Z : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,r : ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) RightModStr over FS : ( ( ) ( ) 1-sorted ) ) -> non empty strict ;
end;

definition
let FS be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let RMS be ( ( non empty ) ( non empty ) RightModStr over FS : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ;
mode Scalar of RMS is ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
mode Vector of RMS is ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let FS1, FS2 be ( ( ) ( ) 1-sorted ) ;
attr c3 is strict ;
struct BiModStr over FS1,FS2 -> ( ( ) ( ) VectSpStr over FS1 : ( ( ) ( ) 1-sorted ) ) , ( ( ) ( ) RightModStr over FS2 : ( ( ) ( ) 1-sorted ) ) ;
aggr BiModStr(# carrier, addF, ZeroF, lmult, rmult #) -> ( ( strict ) ( strict ) BiModStr over FS1 : ( ( ) ( ) 1-sorted ) ,FS2 : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let FS1, FS2 be ( ( ) ( ) 1-sorted ) ;
cluster non empty for ( ( ) ( ) BiModStr over FS1 : ( ( ) ( ) 1-sorted ) ,FS2 : ( ( ) ( ) 1-sorted ) ) ;
end;

registration
let FS1, FS2 be ( ( ) ( ) 1-sorted ) ;
let A be ( ( non empty ) ( non empty ) set ) ;
let a be ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) BinOp of A : ( ( non empty ) ( non empty ) set ) ) ;
let Z be ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ;
let l be ( ( V6() V18([: the carrier of FS1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([: the carrier of FS1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Function of [: the carrier of FS1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ;
let r be ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Function of [:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ;
cluster BiModStr(# A : ( ( non empty ) ( non empty ) set ) ,a : ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:A : ( ( non empty ) ( non empty ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,Z : ( ( ) ( ) Element of A : ( ( non empty ) ( non empty ) set ) ) ,l : ( ( V6() V18([: the carrier of FS1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([: the carrier of FS1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of FS1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,r : ( ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:A : ( ( non empty ) ( non empty ) set ) , the carrier of FS2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,A : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) BiModStr over FS1 : ( ( ) ( ) 1-sorted ) ,FS2 : ( ( ) ( ) 1-sorted ) ) -> non empty strict ;
end;

definition
let R be ( ( non empty right_complementable Abelian add-associative right_zeroed ) ( non empty right_complementable Abelian add-associative right_zeroed ) addLoopStr ) ;
func AbGr R -> ( ( non empty strict right_complementable Abelian add-associative right_zeroed ) ( non empty strict right_complementable Abelian add-associative right_zeroed ) AbGroup) equals :: VECTSP_2:def 4
 addLoopStr(# the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the addF of R : ( ( ) ( ) 1-sorted ) : ( ( V6() V18([: the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( V6() V18([: the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of bool [:[: the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,(0. R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) Element of the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( strict ) addLoopStr ) ;
end;

registration
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster non empty right_complementable strict Abelian add-associative right_zeroed for ( ( ) ( ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
func LeftModule R -> ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) equals :: VECTSP_2:def 5
 VectSpStr(# the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the addF of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,(0. R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( V46(R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) , the multF of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

registration
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster non empty right_complementable Abelian add-associative right_zeroed strict for ( ( ) ( ) RightModStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
func RightModule R -> ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) equals :: VECTSP_2:def 6
 RightModStr(# the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the addF of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,(0. R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( V46(R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) , the multF of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( V6() V18([: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) RightModStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let R be ( ( non empty ) ( non empty ) 1-sorted ) ;
let V be ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
let v be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func v * x -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: VECTSP_2:def 7
 the rmult of V : ( ( ) ( ) 1-sorted ) : ( ( V6() V18([: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) ( V6() V18([: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Function of [: the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) , the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) . (v : ( ( V6() V18([:x : ( ( non empty ) ( non empty ) set ) ,x : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,x : ( ( non empty ) ( non empty ) set ) ) ) ( V6() V18([:x : ( ( non empty ) ( non empty ) set ) ,x : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,x : ( ( non empty ) ( non empty ) set ) ) ) Element of bool [:[:x : ( ( non empty ) ( non empty ) set ) ,x : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,x : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,x : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ;
end;

registration
let R1, R2 be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster non empty right_complementable Abelian add-associative right_zeroed strict for ( ( ) ( ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let R1, R2 be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
func BiModule (R1,R2) -> ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) equals :: VECTSP_2:def 8
 BiModStr(# 1 : ( ( ) ( non empty ) set ) ,op2 : ( ( V6() V18([:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) ) ) ( V6() V18([:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) ) ) Element of bool [:[:1 : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,op0 : ( ( ) ( empty ) Element of 1 : ( ( ) ( non empty ) set ) ) ,(pr2 ( the carrier of R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) )) : ( ( V6() V18([: the carrier of R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) ) ) ( V6() V18([: the carrier of R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,(pr1 (1 : ( ( ) ( non empty ) set ) , the carrier of R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) )) : ( ( V6() V18([:1 : ( ( ) ( non empty ) set ) , the carrier of R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) ) ) ( V6() V18([:1 : ( ( ) ( non empty ) set ) , the carrier of R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) ) ) Element of bool [:[:1 : ( ( ) ( non empty ) set ) , the carrier of R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) ,1 : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) #) : ( ( strict ) ( non empty strict ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

theorem :: VECTSP_2:23
for R being ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring)
for x, y being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * (v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) + w : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) + (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * w : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) + (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & (1. R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (LeftModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) ;

registration
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed for ( ( ) ( ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
mode LeftMod of R is ( ( 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 ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

registration
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster LeftModule R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( non empty right_complementable strict Abelian add-associative right_zeroed ) ( non empty right_complementable strict Abelian add-associative right_zeroed ) VectSpStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) -> non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ;
end;

theorem :: VECTSP_2:24
for R being ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring)
for x, y being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( right_complementable ) Vector of (RightModule R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) holds
( (v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) + w : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) + (w : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) + (v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * (1_ R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) Vector of (RightModule b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) ;

definition
let R be ( ( non empty ) ( non empty ) doubleLoopStr ) ;
let IT be ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ;
attr IT is RightMod-like means :: VECTSP_2:def 9
 for x, y being ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( ) Vector of IT : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) holds
( (v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) + w : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of IT : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) + (w : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of IT : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * (x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) + (v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of IT : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * (y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * y : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) * x : ( ( ) ( ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) * (1_ R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( right_complementable ) Element of the carrier of R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) RightModStr over R : ( ( non empty ) ( non empty ) doubleLoopStr ) ) ) );
end;

registration
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like for ( ( ) ( ) RightModStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
mode RightMod of R is ( ( 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 distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

registration
let R be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster RightModule R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) RightModStr over R : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) -> non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like ;
end;

definition
let R1, R2 be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
let IT be ( ( non empty ) ( non empty ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ;
attr IT is BiMod-like means :: VECTSP_2:def 10
 for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v being ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) set ) ) holds x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * (v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of IT : ( ( non empty ) ( non empty ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

registration
let R1, R2 be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed strict RightMod-like BiMod-like for ( ( ) ( ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

definition
let R1, R2 be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
mode BiMod of R1,R2 is ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed RightMod-like BiMod-like ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed RightMod-like BiMod-like ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ;
end;

theorem :: VECTSP_2:25
for R1, R2 being ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring)
for V being ( ( non empty ) ( non empty ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) holds
( ( for x, y being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for p, q being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( ) Vector of V : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) holds
( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * (v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) + w : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) + (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * w : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) + (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * (y : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & (1_ R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) & (v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) + w : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (w : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * (p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) + q : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + (v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * q : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * (q : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * q : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * (1_ R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) & x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * (v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) * v : ( ( ) ( ) Vector of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) * p : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) iff ( V : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) is RightMod-like & V : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) is vector-distributive & V : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) is scalar-distributive & V : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) is scalar-associative & V : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) is scalar-unital & V : ( ( non empty ) ( non empty ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) is BiMod-like ) ) ;

theorem :: VECTSP_2:26
for R1, R2 being ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) holds BiModule (R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) BiModStr over b1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,b2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) is ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed RightMod-like BiMod-like ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed RightMod-like BiMod-like ) BiMod of R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ;

registration
let R1, R2 be ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ;
cluster BiModule (R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( non empty right_complementable Abelian add-associative right_zeroed strict ) ( non empty right_complementable Abelian add-associative right_zeroed strict ) BiModStr over R1 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ,R2 : ( ( non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) -> non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed strict RightMod-like BiMod-like ;
end;

theorem :: VECTSP_2:27
for L being ( ( non empty ) ( non empty ) multLoopStr ) st L : ( ( non empty ) ( non empty ) multLoopStr ) is well-unital holds
1. L : ( ( non empty ) ( non empty ) multLoopStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) multLoopStr ) : ( ( ) ( non empty ) set ) ) = 1_ L : ( ( non empty ) ( non empty ) multLoopStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) multLoopStr ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: VECTSP_2:28
for K being ( ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) doubleLoopStr )
for a being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) * (- (1. K : ( ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) = - a : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) ( non empty right_complementable right-distributive right_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VECTSP_2:29
for K being ( ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) doubleLoopStr )
for a being ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) holds (- (1. K : ( ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) * a : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) = - a : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) ( non empty right_complementable left-distributive left_unital add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VECTSP_2:30
for F being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) )
for V being ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) )
for v being ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( V46(b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) right_complementable ) Element of the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) iff ( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty non trivial ) set ) ) or v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( V46(b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) right_complementable ) Element of the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: VECTSP_2:31
for F being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) )
for V being ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) )
for v being ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty non trivial ) set ) ) holds
(x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty non trivial ) set ) ) * (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) * v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b3 : ( ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) ( non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital add-associative right_zeroed ) VectSpStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) Vector of ( ( ) ( non empty ) set ) ) ;

theorem :: VECTSP_2:32
for R being ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr )
for V being ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over R : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) )
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v being ( ( ) ( right_complementable ) Vector of V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) holds
( v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * (0. R : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( V46(b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( V46(b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) & v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * (- (1_ R : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = - v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) & (0. V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) : ( ( ) ( V46(b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( V46(b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: VECTSP_2:33
for R being ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr )
for V being ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over R : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) )
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( right_complementable ) Vector of V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) holds
( - (v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * (- x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) & w : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) - (v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) = w : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) + (v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * (- x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: VECTSP_2:34
for R being ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr )
for V being ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over R : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) )
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v being ( ( ) ( right_complementable ) Vector of V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) holds (- v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = - (v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VECTSP_2:35
for R being ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr )
for V being ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over R : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) )
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) )
for v, w being ( ( ) ( right_complementable ) Vector of V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) holds (v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) - w : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = (v : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) - (w : ( ( ) ( right_complementable ) Vector of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( right_complementable ) Element of the carrier of b2 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty right_complementable associative right_unital well-unital distributive Abelian add-associative right_zeroed ) ( non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) doubleLoopStr ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VECTSP_2:36
for F being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) )
for V being ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) )
for v being ( ( ) ( right_complementable ) Vector of V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) holds
( v : ( ( ) ( right_complementable ) Vector of b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = 0. V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( V46(b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) right_complementable ) Element of the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) iff ( x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) = 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty non trivial ) set ) ) or v : ( ( ) ( right_complementable ) Vector of b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) = 0. V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( V46(b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) right_complementable ) Element of the carrier of b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: VECTSP_2:37
for F being ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring)
for x being ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) )
for V being ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) )
for v being ( ( ) ( right_complementable ) Vector of V : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) st x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) <> 0. F : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( V46(b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty non trivial ) set ) ) holds
(v : ( ( ) ( right_complementable ) Vector of b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) * x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) * (x : ( ( ) ( right_complementable ) Scalar of ( ( ) ( non empty non trivial ) set ) ) ") : ( ( ) ( right_complementable ) Element of the carrier of b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) : ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( right_complementable ) Element of ( ( ) ( non empty ) set ) ) = v : ( ( ) ( right_complementable ) Vector of b3 : ( ( non empty right_complementable add-associative right_zeroed RightMod-like ) ( non empty right_complementable add-associative right_zeroed RightMod-like ) RightModStr over b1 : ( ( non empty non degenerated right_complementable almost_left_invertible associative well-unital distributive Abelian add-associative right_zeroed ) ( non empty non degenerated non trivial right_complementable almost_left_invertible unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed ) Ring) ) ) ;