let p be bag of SetPrimes ; :: thesis: for n being non zero Nat st p is prime-factorization-like & n = Product p holds
ppf n = p
let n be non zero Nat; :: thesis: ( p is prime-factorization-like & n = Product p implies ppf n = p )
assume that
A1: p is prime-factorization-like and
A2: n = Product p ; :: thesis: ppf n = p
Product (ppf n) = Product p by A2, NAT_3:61;
hence ppf n = p by A1, Th15; :: thesis: verum