theorem Th43: :: NAT_4:44

for a being Element of NAT
for X being included_in_Seg set
for F being FinSequence of SetPrimes
for p being Prime st X c= SetPrimes & 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 ) )