for p being Prime
for f1, f2 being FinSequence of NAT holds p |-count (f1 ^ f2) = (p |-count f1) ^ (p |-count f2)