theorem Th3: :: NUMBER16:3
for a, b, d, s being Nat st b > 0 & d > 1 & s > 0 holds
ex m, i being Nat st (digits (((ArProg (a,b)) . m),d)) /^ i = digits (s,d)