theorem :: NUMERAL1:10

for n being Nat holds
( 5 divides n iff 5 divides (digits (n,10)) . 0 )