take S = Trivial-Z_ModuleStruct ; :: thesis:
thus S is strict ; :: thesis:
thus S is Abelian ; :: thesis:
thus S is add-associative ; :: thesis:
thus S is right_zeroed ; :: thesis:
thus S is right_complementable ; :: thesis:
thus for a, b being Integer
for v being VECTOR of S holds (a + b) * v = (a * v) + (b * v) by STRUCT_0:def 10; :: according to ZMODUL01:def 3 :: thesis:
thus for a being Integer
for v, w being VECTOR of S holds a * (v + w) = (a * v) + (a * w) by STRUCT_0:def 10; :: according to ZMODUL01:def 2 :: thesis:
thus for a, b being Integer
for v being VECTOR of S holds (a * b) * v = a * (b * v) by STRUCT_0:def 10; :: according to ZMODUL01:def 4 :: thesis:
thus for v being VECTOR of S holds 1 * v = v by STRUCT_0:def 10; :: according to ZMODUL01:def 5 :: thesis: