let p be bag of SetPrimes ; :: thesis: ( p is prime-factorization-like implies ( Product p = 1 iff support p = {} ) )
assume A1: p is prime-factorization-like ; :: thesis: ( Product p = 1 iff support p = {} )

A2: now

assume A3: Product p = 1 ; :: thesis: support p = {}
thus support p = {} :: thesis: verum

proof

assume support p <> {} ; :: thesis: contradiction
then consider q being set such that
A4: q in support p by XBOOLE_0:def 1;
q in SetPrimes by A4;
then reconsider q = q as Element of NAT ;
reconsider q = q as Prime by A4, NEWTON:def 6;
q divides Product p by A1, A4, Lm4;
then q = 1 by A3, WSIERP_1:20;
hence contradiction by INT_2:def 5; :: thesis: verum

end;

end;

now

assume A5: support p = {} ; :: thesis: Product p = 1
consider f being FinSequence of COMPLEX such that
A6: ( Product p = Product f & f = p * (canFS (support p)) ) by NAT_3:def 5;
A7: rng p c= NAT by VALUED_0:def 6;
rng f c= rng p by A6, RELAT_1:45;
then rng f c= NAT by A7, XBOOLE_1:1;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
len (canFS (support p)) = 0 by A5, CARD_1:47, UPROOTS:5;
then canFS (support p) = {} ;
then f = {} by A6;
hence Product p = 1 by A6, RVSUM_1:124; :: thesis: verum

end;

hence ( Product p = 1 iff support p = {} ) by A2; :: thesis: verum