theorem :: COUNTERS:22

for N, M, K being ExtNat holds K * (N + M) = (K * N) + (K * M)