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₁[ FinSequence of NAT ] means for b being Nat st b in dom $1 holds
a divides $1 . b;
defpred S₂[ FinSequence of NAT ] means a divides Sum $1;
defpred S₃[ FinSequence of NAT ] means ( S₁[$1] implies S₂[$1] );

A1: now

let fp be FinSequence of NAT ; :: thesis: for d being Element of NAT st S₃[fp] holds
S₃[fp ^ <*d*>]
let d be Element of NAT ; :: thesis: ( S₃[fp] implies S₃[fp ^ <*d*>] )
assume A2: S₃[fp] ; :: thesis: S₃[fp ^ <*d*>]
set fp1 = fp ^ <*d*>;

now

assume A3: S₁[fp ^ <*d*>] ; :: thesis: S₂[fp ^ <*d*>]
A4: S₁[fp]

proof

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;

len (fp ^ <*d*>) in dom (fp ^ <*d*>) by FINSEQ_5:6;
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₂[fp ^ <*d*>] by RVSUM_1:74; :: thesis: verum

end;

hence S₃[fp ^ <*d*>] ; :: thesis: verum

end;

A6: S₃[ <*> NAT] by NAT_D:6, RVSUM_1:72;
for fp being FinSequence of NAT holds S₃[fp] from FINSEQ_2:sch 2(A6, A1);
hence ( ( for b being Nat st b in dom fp holds
a divides fp . b ) implies a divides Sum fp ) ; :: thesis: verum