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

let n be Nat; :: 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:
per cases ( len d = 0 or len d > 0 ) ;
suppose len d = 0 ; :: 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 S1[ Nat] means ( \$1 < len d implies n divides f . \$1 );
A6: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
thus S1[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) = 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 ; :: thesis: verum
end;
end;
reconsider ld = (len d) - 1 as Element of NAT by ;
A10: ld < len d by XREAL_1:147;
0 in Segm (len d) by ;
then A11: S1[ 0 ] by A1, A3;
A12: addnat "**" d = Sum d by AFINSQ_2:51;
for k being Nat holds S1[k] from NAT_1:sch 2(A11, A6);
hence n divides Sum d by A5, A10, A12; :: thesis: verum
end;
end;