theorem Th83: :: NUMBER14:83

for k, m being Nat holds card ((multiples 2) /\ (seq (k,(2 * m)))) = m