set W = RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #);
A1: for a being Scalar of R
for v, w being Vector of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #)
for v', w' being Vector of V st v = v' & w = w' holds
( v + w = v' + w' & v * a = v' * a ) ;
A2: ( RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is Abelian & RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is add-associative & RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is right_zeroed & RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is right_complementable )

proof

thus RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is Abelian :: thesis: ( RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is add-associative & RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is right_zeroed & RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is right_complementable )

proof

let x, y be Element of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #); :: according to RLVECT_1:def 5 :: thesis: x + y = y + x
reconsider x' = x, y' = y as Vector of V ;
thus x + y = y' + x' by A1
.= y + x ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is right_zeroed & RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is right_complementable )

let x, y, z be Element of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #); :: thesis: (x + y) + z = x + (y + z)
reconsider x' = x, y' = y, z' = z as Vector of V ;
thus (x + y) + z = (x' + y') + z'
.= x' + (y' + z') by RLVECT_1:def 6
.= x + (y + z) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is right_complementable

let x be Element of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #); :: thesis: x + (0. RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #)) = x
reconsider x' = x as Vector of V ;
thus x + (0. RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #)) = x' + (0. V)
.= x by RLVECT_1:10 ; :: thesis: verum

end;

let x be Element of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x' = x as Vector of V ;
consider b being Vector of V such that
A3: x' + b = 0. V by ALGSTR_0:def 11;
reconsider b' = b as Element of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) ;
take b' ; :: according to ALGSTR_0:def 11 :: thesis: x + b' = 0. RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #)
thus x + b' = 0. RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) by A3; :: thesis: verum

end;

RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is RightMod-like

proof

let x, y be Element of R; :: according to VECTSP_2:def 23 :: thesis: for b₁, b₂ being Element of the carrier of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) holds
( (b₁ + b₂) * x = (b₁ * x) + (b₂ * x) & b₁ * (x + y) = (b₁ * x) + (b₁ * y) & b₁ * (y * x) = (b₁ * y) * x & b₁ * (1_ R) = b₁ )
let v, w be Element of RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #); :: thesis: ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
reconsider v' = v, w' = w as Vector of V ;
thus (v + w) * x = (v' + w') * x
.= (v' * x) + (w' * x) by VECTSP_2:def 23
.= (v * x) + (w * x) ; :: thesis: ( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (x + y) = v' * (x + y)
.= (v' * x) + (v' * y) by VECTSP_2:def 23
.= (v * x) + (v * y) ; :: thesis: ( v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (y * x) = v' * (y * x)
.= (v' * y) * x by VECTSP_2:def 23
.= (v * y) * x ; :: thesis: v * (1_ R) = v
thus v * (1_ R) = v' * (1_ R)
.= v by VECTSP_2:def 23 ; :: thesis: verum

end;

then reconsider W = RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) as RightMod of R by A2;
W is Submodule of V

proof

thus ( the carrier of W c= the carrier of V & 0. W = 0. V ) ; :: according to RMOD_2:def 2 :: thesis: ( the addF of W = the addF of V | [:the carrier of W,the carrier of W:] & the rmult of W = the rmult of V | [:the carrier of W,the carrier of R:] )
thus ( the addF of W = the addF of V | [:the carrier of W,the carrier of W:] & the rmult of W = the rmult of V | [:the carrier of W,the carrier of R:] ) by RELSET_1:34; :: thesis: verum

end;

hence RightModStr(# the carrier of V,the addF of V,the U2 of V,the rmult of V #) is strict Submodule of V ; :: thesis: verum