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: n divides Sum d

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: n divides Sum d

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

end;

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

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_{1}[ Nat] means ( $1 < len d implies n divides f . $1 );

A10: ld < len d by XREAL_1:147;

0 in Segm (len d) by A2, NAT_1:44;

then A11: S_{1}[ 0 ]
by A1, A3;

A12: addnat "**" d = Sum d by AFINSQ_2:51;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A11, A6);

hence n divides Sum d by A5, A10, A12; :: thesis: verum

end;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

A6: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

reconsider ld = (len d) - 1 as Element of NAT by A2, NAT_1:20;S

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A7: S

thus S

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 A7, A8, A9, NAT_1:13, NAT_D:8; :: thesis: verum

end;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: verum

A10: ld < len d by XREAL_1:147;

0 in Segm (len d) by A2, NAT_1:44;

then A11: S

A12: addnat "**" d = Sum d by AFINSQ_2:51;

for k being Nat holds S

hence n divides Sum d by A5, A10, A12; :: thesis: verum