let a be Nat; :: thesis: ( 10 divides (a |^ 10) + 1 iff ex r, k being Nat st
( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 ) )
thus ( 10 divides (a |^ 10) + 1 implies ex r, k being Nat st
( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 ) ) :: thesis: ( ex r, k being Nat st
( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 ) implies 10 divides (a |^ 10) + 1 )

proof

assume A1: 10 divides (a |^ 10) + 1 ; :: thesis: ex r, k being Nat st
( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 )
take r = a mod 10; :: thesis: ex k being Nat st
( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 )
take k = a div 10; :: thesis: ( a = (10 * k) + r & 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 )
thus a = (10 * k) + r by NAT_D:2; :: thesis: ( 10 divides (r |^ 10) + 1 & not not r = 0 & ... & not r = 9 )
thus 10 divides (r |^ 10) + 1 by A1, Th29; :: thesis: not not r = 0 & ... & not r = 9
thus not not r = 0 & ... & not r = 9 by NUMPOLY1:8; :: thesis: verum

end;

given r, k being Nat such that A2: a = (10 * k) + r and
A3: 10 divides (r |^ 10) + 1 and
A4: not not r = 0 & ... & not r = 9 ; :: thesis: 10 divides (a |^ 10) + 1
r = a mod 10 by A2, A4, NAT_D:def 2;
hence 10 divides (a |^ 10) + 1 by A3, Th29; :: thesis: verum