set M = the lmult of V;
set W = VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #);
A1: for a, b being Element of VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #)
for x, y being Element of V st x = a & b = y holds
a + b = x + y ;
A2: ( VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is Abelian & VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is add-associative & VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is right_complementable )

proof

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

proof

let a, b be Element of VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #); :: according to RLVECT_1:def 5 :: thesis: a + b = b + a
reconsider x = a, y = b as Element of V ;
thus a + b = y + x by A1
.= b + a ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is right_complementable )

let a, b, c be Element of VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #); :: thesis: (a + b) + c = a + (b + c)
reconsider x = a, y = b, z = c as Element 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: VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is right_complementable

let a be Element of VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #); :: thesis: a + (0. VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #)) = a
reconsider x = a as Element of V ;
thus a + (0. VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #)) = x + (0. V)
.= a by RLVECT_1:10 ; :: thesis: verum

end;

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

end;

VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) is VectSp-like

proof

let a, b be Element of GF; :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) holds
( a * (b₁ + b₂) = (a * b₁) + (a * b₂) & (a + b) * b₁ = (a * b₁) + (b * b₁) & (a * b) * b₁ = a * (b * b₁) & (1. GF) * b₁ = b₁ )
let v, w be Element of VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #); :: thesis: ( a * (v + w) = (a * v) + (a * w) & (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. GF) * v = v )
reconsider x = v, y = w as Element of V ;
thus a * (v + w) = a * (x + y)
.= (a * x) + (a * y) by VECTSP_1:def 26
.= (a * v) + (a * w) ; :: thesis: ( (a + b) * v = (a * v) + (b * v) & (a * b) * v = a * (b * v) & (1. GF) * v = v )
thus (a + b) * v = (a + b) * x
.= (a * x) + (b * x) by VECTSP_1:def 26
.= (a * v) + (b * v) ; :: thesis: ( (a * b) * v = a * (b * v) & (1. GF) * v = v )
thus (a * b) * v = (a * b) * x
.= a * (b * x) by VECTSP_1:def 26
.= a * (b * v) ; :: thesis: (1. GF) * v = v
thus (1. GF) * v = (1_ GF) * x
.= v by VECTSP_1:def 26 ; :: thesis: verum

end;

then reconsider W = VectSpStr(# the carrier of V,the addF of V,(0. V),the lmult of V #) as non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF by A2;
A3: 0. W = 0. V ;
( the addF of W = the addF of V || the carrier of W & the lmult of W = the lmult of V | [:the carrier of GF,the carrier of W:] ) by RELSET_1:34;
then reconsider W = W as Subspace of V by A3, Def2;
take W ; :: thesis: W is strict
thus W is strict ; :: thesis: verum