for d being XFinSequence of NAT
for n being Nat st ( for i being Nat st i in dom d holds
n divides d . i ) holds
n divides Sum d