let d be XFinSequence of NAT ; :: thesis:
let n be Nat; :: thesis:
assume A1: for i being Nat st i in dom d holds
n divides d . i ; :: thesis:

suppose len d = 0 ; :: thesis:

then d = {} ;
then Sum d = 0 ;
hence n divides Sum d by NAT_D:6; :: thesis:

end;

suppose A2: len d > 0 ; :: thesis:

then consider f being sequence of NAT such that
A3: f . 0 = d . 0 and
A4: for n being Nat st n + 1 < len d holds
f . (n + 1) = addnat . ((f . n),(d . (n + 1))) and
A5: addnat "**" 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:

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

assume A8: k + 1 < len d ; :: thesis:
then k + 1 in Segm (len d) by NAT_1:44;
then A9: n divides d . (k + 1) by A1;
f . (k + 1) = addnat . ((f . k),(d . (k + 1))) by A4, A8
.= (f . k) + (d . (k + 1)) by BINOP_2:def 23 ;
hence n divides f . (k + 1) by A7, A8, A9, NAT_1:13, NAT_D:8; :: thesis:

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 (len d) by A2, NAT_1:44;
then A11: S₁[ 0 ] by A1, A3;
A12: addnat "**" d = Sum d by AFINSQ_2:51;
for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A6);
hence n divides Sum d by A5, A10, A12; :: thesis:

end;

end;