theorem :: NUMERAL2:43

for n being Nat holds
( 11 divides n iff 11 divides (Sum (SubXFinS ((digits (n,10)),EvenNAT))) - (Sum (SubXFinS ((digits (n,10)),OddNAT))) )