theorem :: NUMBER17:56
for s being Nat ex n being Nat st
( Sum (digits (n,10)) = s & s divides n )