for fp being FinSequence of NAT
for a being Nat
for b being Element of NAT st a in dom fp & b in dom fp & a <> b & len fp >= 1 holds
fp . b divides Product (Del (fp,a))