let n be Nat; :: thesis: ( 3 divides n iff 3 divides Sum (digits n,10) )
consider p being XFinSequence of such that
A1: ( dom p = dom (digits n,10) & ( for i being Nat st i in dom p holds
p . i = ((digits n,10) . i) * (10 |^ i) ) & value (digits n,10),10 = Sum p ) by Def1;
defpred S₁[ set , set ] means $2 = (p . $1) mod 3;
reconsider dop = dom p as Element of NAT by ORDINAL1:def 13;
A2: for k being Element of NAT st k in dop holds
ex x being Element of NAT st S₁[k,x] ;
consider p' being XFinSequence of such that
A3: ( dom p' = dop & ( for k being Element of NAT st k in dop holds
S₁[k,p' . k] ) ) from STIRL2_1:sch 6(A2);
A4: for i being Nat st i in dom p holds
p' . i = (p . i) mod 3 by A3;

A5: now

let i be Nat; :: thesis: ( i in dom p implies p' . i = ((digits n,10) . i) mod 3 )
reconsider dz = (10 |^ i) - 1 as Nat by NAT_1:20, NEWTON:102;
reconsider dz = dz as Element of NAT by ORDINAL1:def 13;
( 3 divides 3 * 3 & 9 divides dz ) by Th9, NAT_D:def 3;
then 3 divides dz by NAT_D:4;
then 3 divides ((digits n,10) . i) * dz by NAT_D:9;
then A6: (((digits n,10) . i) * dz) mod 3 = 0 by PEPIN:6;
assume A7: i in dom p ; :: thesis: p' . i = ((digits n,10) . i) mod 3
hence p' . i = (p . i) mod 3 by A3
.= (((digits n,10) . i) * (dz + 1)) mod 3 by A1, A7
.= ((((digits n,10) . i) * dz) + ((digits n,10) . i)) mod 3
.= (0 + ((digits n,10) . i)) mod 3 by A6, NAT_D:22
.= ((digits n,10) . i) mod 3 ;
:: thesis: verum

end;

thus ( 3 divides n implies 3 divides Sum (digits n,10) ) :: thesis: ( 3 divides Sum (digits n,10) implies 3 divides n )

proof

assume 3 divides n ; :: thesis: 3 divides Sum (digits n,10)
then 3 divides Sum p by A1, Th8;
then (Sum p) mod 3 = 0 by PEPIN:6;
then (Sum p') mod 3 = 0 by A3, A4, Th6;
then (Sum (digits n,10)) mod 3 = 0 by A1, A3, A5, Th6;
hence 3 divides Sum (digits n,10) by PEPIN:6; :: thesis: verum

end;

assume 3 divides Sum (digits n,10) ; :: thesis: 3 divides n
then (Sum (digits n,10)) mod 3 = 0 by PEPIN:6;
then (Sum p') mod 3 = 0 by A1, A3, A5, Th6;
then (Sum p) mod 3 = 0 by A3, A4, Th6;
then 3 divides Sum p by PEPIN:6;
hence 3 divides n by A1, Th8; :: thesis: verum