let fp be FinSequence of NAT ; :: thesis: for a being Nat st ( for b being Nat st b in dom fp holds

a divides fp . b ) holds

a divides Sum fp

let a be Nat; :: thesis: ( ( for b being Nat st b in dom fp holds

a divides fp . b ) implies a divides Sum fp )

defpred S_{1}[ FinSequence of NAT ] means for b being Nat st b in dom $1 holds

a divides $1 . b;

defpred S_{2}[ FinSequence of NAT ] means a divides Sum $1;

defpred S_{3}[ set ] means ex f being FinSequence of NAT st

( f = $1 & ( S_{1}[f] implies S_{2}[f] ) );

_{3}[ <*> NAT]
by NAT_D:6, RVSUM_1:72;

for fp being FinSequence of NAT holds S_{3}[fp]
from FINSEQ_2:sch 2(A6, A1);

then ex f being FinSequence of NAT st

( f = fp & ( S_{1}[f] implies S_{2}[f] ) )
;

hence ( ( for b being Nat st b in dom fp holds

a divides fp . b ) implies a divides Sum fp ) ; :: thesis: verum

a divides fp . b ) holds

a divides Sum fp

let a be Nat; :: thesis: ( ( for b being Nat st b in dom fp holds

a divides fp . b ) implies a divides Sum fp )

defpred S

a divides $1 . b;

defpred S

defpred S

( f = $1 & ( S

A1: now :: thesis: for fp being FinSequence of NAT

for d being Element of NAT st S_{3}[fp] holds

S_{3}[fp ^ <*d*>]

A6:
Sfor d being Element of NAT st S

S

let fp be FinSequence of NAT ; :: thesis: for d being Element of NAT st S_{3}[fp] holds

S_{3}[fp ^ <*d*>]

let d be Element of NAT ; :: thesis: ( S_{3}[fp] implies S_{3}[fp ^ <*d*>] )

assume A2: S_{3}[fp]
; :: thesis: S_{3}[fp ^ <*d*>]

set fp1 = fp ^ <*d*>;

_{3}[fp ^ <*d*>]
; :: thesis: verum

end;S

let d be Element of NAT ; :: thesis: ( S

assume A2: S

set fp1 = fp ^ <*d*>;

now :: thesis: ( S_{1}[fp ^ <*d*>] implies S_{2}[fp ^ <*d*>] )

hence
Sassume A3:
S_{1}[fp ^ <*d*>]
; :: thesis: S_{2}[fp ^ <*d*>]

A4: S_{1}[fp]

then a divides (fp ^ <*d*>) . (len (fp ^ <*d*>)) by A3;

then a divides (fp ^ <*d*>) . ((len fp) + 1) by FINSEQ_2:16;

then a divides d by FINSEQ_1:42;

then a divides (Sum fp) + d by A2, A4, NAT_D:8;

hence S_{2}[fp ^ <*d*>]
by RVSUM_1:74; :: thesis: verum

end;A4: S

proof

len (fp ^ <*d*>) in dom (fp ^ <*d*>)
by FINSEQ_5:6;
let b be Nat; :: thesis: ( b in dom fp implies a divides fp . b )

assume A5: b in dom fp ; :: thesis: a divides fp . b

( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . b = fp . b ) by A5, FINSEQ_1:26, FINSEQ_1:def 7;

hence a divides fp . b by A3, A5; :: thesis: verum

end;assume A5: b in dom fp ; :: thesis: a divides fp . b

( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . b = fp . b ) by A5, FINSEQ_1:26, FINSEQ_1:def 7;

hence a divides fp . b by A3, A5; :: thesis: verum

then a divides (fp ^ <*d*>) . (len (fp ^ <*d*>)) by A3;

then a divides (fp ^ <*d*>) . ((len fp) + 1) by FINSEQ_2:16;

then a divides d by FINSEQ_1:42;

then a divides (Sum fp) + d by A2, A4, NAT_D:8;

hence S

for fp being FinSequence of NAT holds S

then ex f being FinSequence of NAT st

( f = fp & ( S

hence ( ( for b being Nat st b in dom fp holds

a divides fp . b ) implies a divides Sum fp ) ; :: thesis: verum