let n be Nat; :: thesis: for p being Prime
for f being bag of SetPrimes st f . p = p |^ n holds
p |^ n divides Product f
let p be Prime; :: thesis: for f being bag of SetPrimes st f . p = p |^ n holds
p |^ n divides Product f
let f be bag of SetPrimes ; :: thesis: ( f . p = p |^ n implies p |^ n divides Product f )
assume AA: f . p = p |^ n ; :: thesis: p |^ n divides Product f
consider g being FinSequence of NAT such that
A2: ( Product f = Product g & g = f * (canFS (support f)) ) by Matsu0;
reconsider PP = Product g as Nat ;
p in SetPrimes by NEWTON:def 6;
then B0: p in dom f by PARTFUN1:def 2;
B1: p in support f by AA, PRE_POLY:def 7;
rng (canFS (support f)) = support f by FUNCT_2:def 3;
then consider y being object such that
B2: ( y in dom (canFS (support f)) & p = (canFS (support f)) . y ) by B1, FUNCT_1:def 3;
B3: y in dom g by A2, FUNCT_1:11, B2, B0;
f . p = g . y by A2, B2, FUNCT_1:13;
then f . p in rng g by FUNCT_1:3, B3;
hence p |^ n divides Product f by A2, AA, NAT_3:7; :: thesis: verum