take V = ModuleStr(# the carrier of F, the addF of F,(0. F), the multF of F #); :: thesis: ( V is scalar-distributive & V is vector-distributive & V is scalar-associative & V is scalar-unital & 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 being Element of V holds (x + y) * v = (x * v) + (y * v) by Lm3; :: according to VECTSP_1:def 14 :: thesis: ( V is vector-distributive & V is scalar-associative & V is scalar-unital & V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus for x being Element of F
for v, w being Element of V holds x * (v + w) = (x * v) + (x * w) by Lm3; :: according to VECTSP_1:def 13 :: thesis: ( V is scalar-associative & V is scalar-unital & 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 being Element of V holds (x * y) * v = x * (y * v) by Lm3; :: according to VECTSP_1:def 15 :: thesis: ( V is scalar-unital & V is add-associative & V is right_zeroed & V is right_complementable & V is Abelian & V is strict )
thus for v being Element of V holds (1. F) * v = v by Lm3; :: according to VECTSP_1:def 16 :: 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 Lm2; :: thesis: verum