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