set W = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #);
A1: RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is RightMod-like

proof

let x, y be Element of R; :: according to VECTSP_2:def 8 :: thesis: for b₁, b₂ being Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF 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 ZeroF 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 v9 = v, w9 = w as Vector of V ;
thus (v + w) * x = (v9 + w9) * x
.= (v9 * x) + (w9 * x) by VECTSP_2:def 9
.= (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) = v9 * (x + y)
.= (v9 * x) + (v9 * y) by VECTSP_2:def 9
.= (v * x) + (v * y) ; :: thesis: ( v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (y * x) = v9 * (y * x)
.= (v9 * y) * x by VECTSP_2:def 9
.= (v * y) * x ; :: thesis: v * (1_ R) = v
thus v * (1_ R) = v9 * (1_ R)
.= v by VECTSP_2:def 9 ; :: thesis: verum

end;

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

proof

thus RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Abelian :: thesis: ( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V, the ZeroF 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 ZeroF of V, the rmult of V #); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider x9 = x, y9 = y as Vector of V ;
thus x + y = y9 + x9 by A2
.= y + x ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V, the ZeroF 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 ZeroF of V, the rmult of V #); :: thesis: (x + y) + z = x + (y + z)
reconsider x9 = x, y9 = y, z9 = z as Vector of V ;
thus (x + y) + z = (x9 + y9) + z9
.= x9 + (y9 + z9) by RLVECT_1:def 3
.= x + (y + z) ; :: thesis: verum

end;

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

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

end;

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

end;

then reconsider W = RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) as RightMod of R by A1;
A4: the rmult of W = the rmult of V | [: the carrier of W, the carrier of R:] by RELSET_1:19;
( 0. W = 0. V & the addF of W = the addF of V | [: the carrier of W, the carrier of W:] ) by RELSET_1:19;
hence RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is strict Submodule of V by A4, Def2; :: thesis: verum