for fp being FinSequence of NAT
for d being Nat st ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) holds
(Product fp) gcd d = 1