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 ; :: 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,(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 ; :: 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 ;
thus (v + w) * a = (x + y) * a
.= (x * a) + (y * a) by VECTSP_2:def 23
.= (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 23
.= (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 23
.= (v * b) * a ; :: thesis: v * (1_ R) = v
thus v * (1_ R) = x * (1_ R)
.= v by VECTSP_2:def 23 ; :: thesis: verum

end;

A2: for a, b being Element of
for x, y being Vector of 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 ; :: according to RLVECT_1:def 5 :: thesis: a + b = b + a
reconsider x = a, y = b as Vector of ;
thus a + b = y + x by A2
.= b + a ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: 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 ; :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Vector of ;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 6
.= a + (b + c) ; :: thesis: verum

end;

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

let a be Element of ; :: 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 ;
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 7 ; :: thesis: verum

end;

let a be Element of ; :: according to ALGSTR_0:def 16 :: thesis: a is right_complementable
reconsider x = a as Vector of ;
reconsider b = (comp V) . x as Element of ;
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 25
.= 0. RightModStr(# the carrier of V,the addF of V,(0. V),the rmult of V #) by RLVECT_1:16 ; :: thesis: verum

end;

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