let d be XFinSequence of INT ; :: thesis: for n being Integer st ( for i being Nat st i in dom d holds
n divides d . i ) holds
n divides Sum d
let n be Integer; :: thesis: ( ( for i being Nat st i in dom d holds
n divides d . i ) implies n divides Sum d )
assume A1: for i being Nat st i in dom d holds
n divides d . i ; :: thesis: n divides Sum d

per cases ( len d = 0 or len d > 0 ) ;

suppose len d = 0 ; :: thesis: n divides Sum d

then d = {} ;
then Sum d = 0 ;
hence n divides Sum d by INT_2:12; :: thesis: verum

end;

suppose A2: len d > 0 ; :: thesis: n divides Sum d

then consider f being Function of NAT,INT such that
A3: f . 0 = d . 0 and
A4: for n being Nat st n + 1 < len d holds
f . (n + 1) = addint . ((f . n),(d . (n + 1))) and
A5: addint "**" d = f . ((len d) - 1) by AFINSQ_2:def 8;
defpred S₁[ Nat] means ( $1 < len d implies n divides f . $1 );

A6: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume A8: k + 1 < len d ; :: thesis: n divides f . (k + 1)
then k + 1 in Segm (len d) by NAT_1:44;
then A9: n divides d . (k + 1) by A1;
f . (k + 1) = addint . ((f . k),(d . (k + 1))) by A4, A8
.= (f . k) + (d . (k + 1)) by BINOP_2:def 20 ;
hence n divides f . (k + 1) by A7, A8, A9, XREAL_1:145, WSIERP_1:4; :: thesis: verum

end;

end;

reconsider ld = (len d) - 1 as Element of NAT by A2, NAT_1:20;
A10: ld < len d by XREAL_1:147;
0 in Segm (dom d) by NAT_1:44, A2;
then A11: S₁[ 0 ] by A1, A3;
A12: addint "**" d = Sum d by AFINSQ_2:50;
for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A6);
hence n divides Sum d by A5, A10, A12; :: thesis: verum

end;

end;