scheme :: NAT_4:sch 3
scheme3{ P₁[ set , set , set ] } :

for p being Prime
for n being Element of NAT
for m being non zero Element of NAT
for X being set st X = { (p9 |^ (p9 |-count m)) where p9 is prime Element of NAT : P₁[n,m,p9] } & p |^ (p |-count m) in X holds
p |-count (Product (Sgm X)) = p |-count m