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 :: thesis: ( Product p = 1 implies support p = {} )
assume A3: Product p = 1 ; :: thesis: support p = {}
thus support p = {} :: thesis: verum
proof
assume support p <> {} ; :: thesis: contradiction
then consider q being object 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 = 1 by A1, A3, A4, Lm4, WSIERP_1:15;
hence contradiction by INT_2:def 4; :: thesis: verum
end;
end;
now :: thesis: ( support p = {} implies Product p = 1 )
consider f being FinSequence of COMPLEX such that
A5: Product p = Product f and
A6: f = p * (canFS (support p)) by NAT_3:def 5;
assume support p = {} ; :: thesis: Product p = 1
hence Product p = 1 by A5, A6, RVSUM_1:94; :: thesis: verum
end;
hence ( Product p = 1 iff support p = {} ) by A2; :: thesis: verum