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