theorem Th156: :: ZMODUL01:156

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a being Element of R
for i, j, k being Element of NAT st i <= j & k = j - i holds
(Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))