let p be bag of ; :: thesis: for n being non empty natural number st p is prime-factorization-like & n = Product p holds
ppf n = p
let n be non empty natural number ; :: thesis: ( p is prime-factorization-like & n = Product p implies ppf n = p )
assume A1: ( p is prime-factorization-like & n = Product p ) ; :: thesis: ppf n = p
Product (ppf n) = Product p by A1, NAT_3:61;
hence ppf n = p by A1, Th15; :: thesis: verum