for p being Prime
for f being FinSequence of NAT st f = {} holds
p |-count f = {}