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