defpred S_{1}[ Nat] means for f being FinSequence of NAT st len f = $1 holds

for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f;

A1: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A1, A3);

let f be FinSequence of NAT ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds

i divides f /. j ) implies i divides Sum f )

assume A16: for j being Element of NAT st j in dom f holds

i divides f /. j ; :: thesis: i divides Sum f

len f = len f ;

hence i divides Sum f by A15, A16; :: thesis: verum

for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f;

A1: S

proof

A3:
for k being Nat st S
let f be FinSequence of NAT ; :: thesis: ( len f = 0 implies for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f )

assume len f = 0 ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f

then A2: f = <*> NAT ;

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds

i divides f /. j ) implies i divides Sum f )

assume for j being Element of NAT st j in dom f holds

i divides f /. j ; :: thesis: i divides Sum f

Sum f = 0 by A2, RVSUM_1:72;

hence i divides Sum f by NAT_D:6; :: thesis: verum

end;i divides f /. j ) holds

i divides Sum f )

assume len f = 0 ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f

then A2: f = <*> NAT ;

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds

i divides f /. j ) implies i divides Sum f )

assume for j being Element of NAT st j in dom f holds

i divides f /. j ; :: thesis: i divides Sum f

Sum f = 0 by A2, RVSUM_1:72;

hence i divides Sum f by NAT_D:6; :: thesis: verum

S

proof

A15:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

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

let f be FinSequence of NAT ; :: thesis: ( len f = k + 1 implies for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f )

assume A5: len f = k + 1 ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds

i divides f /. j ) implies i divides Sum f )

assume A6: for j being Element of NAT st j in dom f holds

i divides f /. j ; :: thesis: i divides Sum f

f <> {} by A5;

then consider q being FinSequence, x being object such that

A7: f = q ^ <*x*> by FINSEQ_1:46;

reconsider f1 = q as FinSequence of NAT by A7, FINSEQ_1:36;

reconsider f2 = <*x*> as FinSequence of NAT by A7, FINSEQ_1:36;

k + 1 = (len f1) + (len f2) by A5, A7, FINSEQ_1:22;

then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39;

for j being Element of NAT st j in dom f1 holds

i divides f1 /. j

rng f2 c= NAT by FINSEQ_1:def 4;

then {x} c= NAT by FINSEQ_1:38;

then reconsider m = x as Element of NAT by ZFMISC_1:31;

A12: f . (len f) = m by A5, A7, A8, FINSEQ_1:42;

len f in Seg (len f) by A5, FINSEQ_1:3;

then A13: len f in dom f by FINSEQ_1:def 3;

then f /. (len f) = f . (len f) by PARTFUN1:def 6;

then A14: i divides m by A6, A12, A13;

Sum f = (Sum f1) + m by A7, RVSUM_1:74;

hence i divides Sum f by A11, A14, NAT_D:8; :: thesis: verum

end;assume A4: S

let f be FinSequence of NAT ; :: thesis: ( len f = k + 1 implies for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f )

assume A5: len f = k + 1 ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds

i divides f /. j ) implies i divides Sum f )

assume A6: for j being Element of NAT st j in dom f holds

i divides f /. j ; :: thesis: i divides Sum f

f <> {} by A5;

then consider q being FinSequence, x being object such that

A7: f = q ^ <*x*> by FINSEQ_1:46;

reconsider f1 = q as FinSequence of NAT by A7, FINSEQ_1:36;

reconsider f2 = <*x*> as FinSequence of NAT by A7, FINSEQ_1:36;

k + 1 = (len f1) + (len f2) by A5, A7, FINSEQ_1:22;

then A8: k + 1 = (len f1) + 1 by FINSEQ_1:39;

for j being Element of NAT st j in dom f1 holds

i divides f1 /. j

proof

then A11:
i divides Sum f1
by A4, A8;
let j be Element of NAT ; :: thesis: ( j in dom f1 implies i divides f1 /. j )

assume A9: j in dom f1 ; :: thesis: i divides f1 /. j

A10: dom f1 c= dom f by A7, FINSEQ_1:26;

then f /. j = f . j by A9, PARTFUN1:def 6

.= f1 . j by A7, A9, FINSEQ_1:def 7

.= f1 /. j by A9, PARTFUN1:def 6 ;

hence i divides f1 /. j by A6, A9, A10; :: thesis: verum

end;assume A9: j in dom f1 ; :: thesis: i divides f1 /. j

A10: dom f1 c= dom f by A7, FINSEQ_1:26;

then f /. j = f . j by A9, PARTFUN1:def 6

.= f1 . j by A7, A9, FINSEQ_1:def 7

.= f1 /. j by A9, PARTFUN1:def 6 ;

hence i divides f1 /. j by A6, A9, A10; :: thesis: verum

rng f2 c= NAT by FINSEQ_1:def 4;

then {x} c= NAT by FINSEQ_1:38;

then reconsider m = x as Element of NAT by ZFMISC_1:31;

A12: f . (len f) = m by A5, A7, A8, FINSEQ_1:42;

len f in Seg (len f) by A5, FINSEQ_1:3;

then A13: len f in dom f by FINSEQ_1:def 3;

then f /. (len f) = f . (len f) by PARTFUN1:def 6;

then A14: i divides m by A6, A12, A13;

Sum f = (Sum f1) + m by A7, RVSUM_1:74;

hence i divides Sum f by A11, A14, NAT_D:8; :: thesis: verum

let f be FinSequence of NAT ; :: thesis: for i being Element of NAT st ( for j being Element of NAT st j in dom f holds

i divides f /. j ) holds

i divides Sum f

let i be Element of NAT ; :: thesis: ( ( for j being Element of NAT st j in dom f holds

i divides f /. j ) implies i divides Sum f )

assume A16: for j being Element of NAT st j in dom f holds

i divides f /. j ; :: thesis: i divides Sum f

len f = len f ;

hence i divides Sum f by A15, A16; :: thesis: verum