let p be bag of ; :: thesis: ( p is prime-factorization-like implies Product p <> 0 )
assume A1: p is prime-factorization-like ; :: thesis: Product p <> 0
consider f being FinSequence of COMPLEX such that
A2: ( Product p = Product f & f = p * (canFS (support p)) ) by NAT_3:def 5;
reconsider f = f as complex-yielding FinSequence ;
assume Product p = 0 ; :: thesis: contradiction
then consider k being Nat such that
A3: ( k in dom f & f . k = 0 ) by A2, RVSUM_1:133;
A4: rng (canFS (support p)) = support p by FUNCT_2:def 3;
k in dom (canFS (support p)) by A2, A3, FUNCT_1:21;
then A5: (canFS (support p)) . k in support p by A4, FUNCT_1:12;
then reconsider q = (canFS (support p)) . k as Prime by NEWTON:def 6;
consider n being natural number such that
A6: ( 0 < n & p . q = q |^ n ) by A1, A5, Def1;
thus contradiction by A2, A3, A6, FUNCT_1:22; :: thesis: verum