take RightModule R ; :: thesis: ( RightModule R is Abelian & RightModule R is add-associative & RightModule R is right_zeroed & RightModule R is right_complementable & RightModule R is RightMod-like & RightModule R is strict )
thus ( RightModule R is Abelian & RightModule R is add-associative & RightModule R is right_zeroed & RightModule R is right_complementable ) ; :: thesis: ( RightModule R is RightMod-like & RightModule R is strict )
thus for x, y being Scalar of R
for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) by Th24; :: according to VECTSP_2:def 8 :: thesis: RightModule R is strict
thus RightModule R is strict ; :: thesis: verum