let A be finite Subset of SetPrimes; :: thesis: Product (A -bag) is square-free
set n = Product (A -bag);
reconsider n = Product (A -bag) as non zero Nat by MOEBIUS2:26;
C2: Product (A -bag) = Product (ppf n) by NAT_3:61;
ZW: ppf n = A -bag by INT_7:15, C2;
for p being Prime holds not p |^ 2 divides n

proof

given p1 being Prime such that K1: p1 |^ 2 divides n ; :: thesis: contradiction
K2: p1 |-count (p1 |^ 2) <= p1 |-count n by NAT_3:30, K1;
set m = p1 |-count n;
W2: p1 |-count n >= 2 by K2, NAT_3:25, INT_2:def 4;
p1 |^ 1 divides p1 |^ 2 by NEWTON:89;
then V1: p1 in support (pfexp n) by NAT_3:37, K1, NAT_D:4;
then W1: (ppf n) . p1 = p1 |^ (p1 |-count n) by NAT_3:def 9;
p1 in support (ppf n) by V1, NAT_3:def 9;
then p1 = p1 |^ (p1 |-count n) by W1, BagValue, ZW;
hence contradiction by PREPOWER:13, W2, INT_2:def 4; :: thesis: verum

end;

hence Product (A -bag) is square-free by MOEBIUS1:def 1; :: thesis: verum