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