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

proof

let a, b be Scalar 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,(0. V), the rmult of V #) holds
( (b₁ + b₂) * a = (b₁ * a) + (b₂ * a) & b₁ * (a + b) = (b₁ * a) + (b₁ * b) & b₁ * (b * a) = (b₁ * b) * a & b₁ * (1_ R) = b₁ )
let v, w be Vector of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); :: thesis: ( (v + w) * a = (v * a) + (w * a) & v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
reconsider x = v, y = w as Vector of V ;
thus (v + w) * a = (x + y) * a
.= (x * a) + (y * a) by VECTSP_2:def 9
.= (v * a) + (w * a) ; :: thesis: ( v * (a + b) = (v * a) + (v * b) & v * (b * a) = (v * b) * a & v * (1_ R) = v )
thus v * (a + b) = x * (a + b)
.= (x * a) + (x * b) by VECTSP_2:def 9
.= (v * a) + (v * b) ; :: thesis: ( v * (b * a) = (v * b) * a & v * (1_ R) = v )
thus v * (b * a) = x * (b * a)
.= (x * b) * a by VECTSP_2:def 9
.= (v * b) * a ; :: thesis: v * (1_ R) = v
thus v * (1_ R) = x * (1_ R)
.= v by VECTSP_2:def 9 ; :: thesis: verum

end;

A2: for a, b being Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
for x, y being Vector of V st x = a & b = y holds
a + b = x + y ;
( RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Abelian & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is add-associative & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_zeroed & RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is right_complementable )

proof

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

proof

let a, b be Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); :: according to RLVECT_1:def 2 :: thesis: a + b = b + a
reconsider x = a, y = b as Vector of V ;
thus a + b = y + x by A2
.= b + a ; :: thesis: verum

end;

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

let a, b, c be Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Vector of V ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 3
.= a + (b + c) ; :: thesis: verum

end;

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

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

end;

let a be Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #); :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Vector of V ;
reconsider b = (comp V) . x as Element of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) ;
take b ; :: according to ALGSTR_0:def 11 :: thesis: a + b = 0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
thus a + b = x + (- x) by VECTSP_1:def 13
.= 0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) by RLVECT_1:5 ; :: thesis: verum

end;

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