for fp being FinSequence of NAT
for a being Nat st ( for b being Nat st b in dom fp holds
a divides fp . b ) holds
a divides Sum fp