set W = VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #);
A1: for a being Element of GF
for v, w being Element of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #)
for v', w' being Element of V st v = v' & w = w' holds
( v + w = v' + w' & a * v = a * v' ) ;
A2: ( VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) is Abelian & VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) is add-associative & VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) is right_zeroed & VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) is right_complementable )

proof

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

proof

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

end;

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

let x, y, z be Element of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #); :: thesis: (x + y) + z = x + (y + z)
reconsider x' = x, y' = y, z' = z as Element of V ;
thus (x + y) + z = (x' + y') + z'
.= x' + (y' + z') by RLVECT_1:def 6
.= x + (y + z) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) is right_complementable

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

end;

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

end;

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

proof

let x, y 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,the U2 of V,the lmult of V #) holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (x + y) * b₁ = (x * b₁) + (y * b₁) & (x * y) * b₁ = x * (y * b₁) & (1. GF) * b₁ = b₁ )
let v, w be Element of VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. GF) * v = v )
reconsider v' = v, w' = w as Element of V ;
thus x * (v + w) = x * (v' + w')
.= (x * v') + (x * w') by VECTSP_1:def 26
.= (x * v) + (x * w) ; :: thesis: ( (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. GF) * v = v )
thus (x + y) * v = (x + y) * v'
.= (x * v') + (y * v') by VECTSP_1:def 26
.= (x * v) + (y * v) ; :: thesis: ( (x * y) * v = x * (y * v) & (1. GF) * v = v )
thus (x * y) * v = (x * y) * v'
.= x * (y * v') by VECTSP_1:def 26
.= x * (y * v) ; :: thesis: (1. GF) * v = v
thus (1. GF) * v = (1_ GF) * v'
.= v by VECTSP_1:def 26 ; :: thesis: verum

end;

then reconsider W = VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) as non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF by A2;
W is Subspace of V

proof

thus ( the carrier of W c= the carrier of V & 0. W = 0. V ) ; :: according to VECTSP_4:def 2 :: thesis: ( 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:] )
thus ( 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; :: thesis: verum

end;

hence VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) is strict Subspace of V ; :: thesis: verum