theorem :: GROUP_1A:47

for L being non empty Abelian add-associative add-unital addMagma
for x, y being Element of L
for n being Nat holds (mult L) . (n,(x + y)) = ((mult L) . (n,x)) + ((mult L) . (n,y))