theorem Th47: :: NUMBER15:47
for s being Nat
for k, n being non zero Nat st k <> n & n <= s & k <= s holds
primenumber (k - 1) divides (sequenceA s) . n