theorem Th43: :: NAT_4:44

for a, k being Element of NAT
for X being set
for F being FinSequence of SetPrimes
for p being Prime st X c= SetPrimes & X c= Seg k & F = Sgm X & a = Product F holds
( ( p in rng F implies p |-count a = 1 ) & ( not p in rng F implies p |-count a = 0 ) )