let i be Nat; :: thesis: not 3 divides ((ArProg (2,3)) . i) - 1
assume 3 divides ((ArProg (2,3)) . i) - 1 ; :: thesis: contradiction
then 3 divides (2 + (3 * i)) - 1 by ArDefNth;
then ( 3 divides 1 + (3 * i) & 3 divides 3 * i ) ;
then 3 divides (1 + (3 * i)) - (3 * i) by PREPOWER:94;
hence contradiction by NAT_D:7; :: thesis: verum