take V = VectSpStr(# the carrier of F,the addF of F,(0. F),the multF of F #); :: thesis: ( V is VectSp-like & V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus for x, y being Element of F
for v, w being Element of V holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. F) * v = v ) by Lm5; :: according to VECTSP_1:def 26 :: thesis: ( V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus ( V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict ) by Lm4; :: thesis: verum