theorem :: ZMODUL01:164

for AG being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds ModuleStr(# the carrier of AG, the addF of AG, the ZeroF of AG,(Int-mult-left AG) #) is Z_Module