:: deftheorem Def1 defines |-count NAT_4:def 1 :
for f being FinSequence of NAT
for p being Prime
for b₃ being FinSequence of NAT holds
( b₃ = p |-count f iff ( len b₃ = len f & ( for i being set st i in dom b₃ holds
b₃ . i = p |-count (f . i) ) ) );