set M = the rmult of V;
set W = RightModStr(# the carrier of V,the addF of V,(0. V),the rmult of V #);
A1: 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 ;
A2: ( 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 5 :: thesis: a + b = b + a
reconsider x = a, y = b as Vector of V ;
thus a + b = y + x by A1
.= 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 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 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 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 7 ; :: 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 25
.= 0. RightModStr(# the carrier of V,the addF of V,(0. V),the rmult of V #) by RLVECT_1:16 ; :: thesis: verum

end;

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 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 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 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;

then reconsider W = RightModStr(# the carrier of V,the addF of V,(0. V),the rmult of V #) as RightMod of R by A2;
A3: 0. W = 0. V ;
( the addF of W = the addF of V || the carrier of W & 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