let n be Nat; :: thesis: for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |-count (Product f) >= n
let p be Prime; :: thesis: for f being bag of SetPrimes st f . p = p |^ n holds
p |-count (Product f) >= n
let f be bag of SetPrimes ; :: thesis: ( f . p = p |^ n implies p |-count (Product f) >= n )
assume AA: f . p = p |^ n ; :: thesis: p |-count (Product f) >= n
Product f <> 0 by Matsu;
hence p |-count (Product f) >= n by Ciek, AA, Matsu1; :: thesis: verum