n:{1...}. 
!f:(Prime
). f is a factorization of nn:{1...}. f:(Prime). f is a factorization of nn:, f,g:(Prime).
Thm* f is a factorization of n
g is a factorization of n f = g| Rank | Theorem | Name |
| 23 | n:{1...}. !f:(Prime). f is a factorization of n | [fta_mset] |
| cites the following: | ||
| 15 | n:{1...}. f:(Prime). f is a factorization of n | [prime_factorization_exists2] |
| 22 | n:, f,g:(Prime).
Thm* f is a factorization of n g is a factorization of n f = g | [prime_factorization_mset_unique] |