let p, q be bag of SetPrimes ; :: thesis: ( support p c= support q & p | (support p) = q | (support p) implies Product p divides Product q )
assume that
A1: support p c= support q and
A2: p | (support p) = q | (support p) ; :: thesis: Product p divides Product q
consider r being bag of SetPrimes such that
support r = (support q) \ (support p) and
A3: support p misses support r and
r | (support r) = q | (support r) and
A4: p + r = q by A1, A2, Lm2;
(Product p) * (Product r) = Product q by A3, A4, NAT_3:19;
hence Product p divides Product q by INT_1:def 3; :: thesis: verum