defpred S1[ 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:
S1[ 0 ]
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
let f be
FinSequence of
NAT ;
( 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
;
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 ;
( ( 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
;
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
then A11:
i divides Sum f1
by A4, A8;
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;
verum
end;
A15:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A3);
let f be FinSequence of NAT ; 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 ; ( ( 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
; i divides Sum f
len f = len f
;
hence
i divides Sum f
by A15, A16; verum