let f be bag of SetPrimes ; :: thesis: Product f <> 0
consider g being FinSequence of COMPLEX such that
A2: ( Product f = Product g & g = f * (canFS (support f)) ) by NAT_3:def 5;
assume Product f = 0 ; :: thesis: contradiction
then consider k being Nat such that
H1: ( k in dom g & g . k = 0 ) by A2, RVSUM_1:103;
h1: dom g c= dom (canFS (support f)) by A2, RELAT_1:25;
then H3: f . ((canFS (support f)) . k) = 0 by A2, H1, FUNCT_1:13;
(canFS (support f)) . k in rng (canFS (support f)) by FUNCT_1:3, H1, h1;
then (canFS (support f)) . k in support f by FUNCT_2:def 3;
hence contradiction by H3, PRE_POLY:def 7; :: thesis: verum