theorem :: NUMBER03:44

for a being Nat holds
( 10 divides (a |^ 10) + 1 iff ex k being Nat st
( a = (10 * k) + 3 or a = (10 * k) + 7 ) )