theorem :: NUMBER16:4

for a, b, s being Nat st b > 0 & s > 0 holds
ex m, i being Nat st (digits (((ArProg (a,b)) . m),10)) /^ i = digits (s,10) by Th3;