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 S1[ FinSequence of NAT ] means for b being Nat st b in dom $1 holds
a divides $1 . b;
defpred S2[ FinSequence of NAT ] means a divides Sum $1;
defpred S3[ set ] means ex f being FinSequence of NAT st
( f = $1 & ( S1[f] implies S2[f] ) );
A1: now :: thesis: for fp being FinSequence of NAT
for d being Element of NAT st S3[fp] holds
S3[fp ^ <*d*>]
let fp be FinSequence of NAT ; :: thesis: for d being Element of NAT st S3[fp] holds
S3[fp ^ <*d*>]
let d be Element of NAT ; :: thesis: ( S3[fp] implies S3[fp ^ <*d*>] )
assume A2: S3[fp] ; :: thesis: S3[fp ^ <*d*>]
set fp1 = fp ^ <*d*>;
now :: thesis: ( S1[fp ^ <*d*>] implies S2[fp ^ <*d*>] )
assume A3: S1[fp ^ <*d*>] ; :: thesis: S2[fp ^ <*d*>]
A4: S1[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 S2[fp ^ <*d*>] by RVSUM_1:74; :: thesis: verum
end;
hence S3[fp ^ <*d*>] ; :: thesis: verum
end;
A6: S3[ <*> NAT] by NAT_D:6, RVSUM_1:72;
for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch 2(A6, A1);
 then ex f being FinSequence of NAT st
( f = fp & ( S1[f] implies S2[f] ) ) ;
hence ( ( for b being Nat st b in dom fp holds
a divides fp . b ) implies a divides Sum fp ) ; :: thesis: verum