unique_factorization: THEORY
BEGIN
 
   IMPORTING prime_factorization, unique_scaf

   fs,fs1,fs2: VAR fseq[posnat]


   n,m: VAR nat
   i,j: VAR int


   FTL_sym: LEMMA (FORALL (k: nat):
       k < j
    IMPLIES
         (FORALL (fs1: fseq[posnat], fs2: fseq[posnat]):
     k = product(fs1)
         AND k = product(fs2)
           AND ordered_list_of_primes?(fs1)
      AND ordered_list_of_primes?(fs2) AND k > 1
         IMPLIES fs1 = fs2))
      AND j = product(fs1) 
      AND j = product(fs2) 
      AND ordered_list_of_primes?(fs1)
      AND ordered_list_of_primes?(fs2)
      AND j > 1
      AND length(fs2) > 1
      AND length(fs1) > 1
      AND seq(fs2)(length(fs2) - 1) < seq(fs1)(length(fs1) - 1)  
    IMPLIES
        fs1 = fs2

   FTL_prep: THEOREM n = product(fs1) AND n = product(fs2) 
                     AND ordered_list_of_primes?(fs1)
                     AND ordered_list_of_primes?(fs2)
                     AND n > 1 
                             IMPLIES fs1 = fs2

   Fundamental_Theorem_Arithmetic: THEOREM n = product(fs1) AND n = product(fs2)
                                           AND ordered_list_of_primes?(fs1)
                                           AND ordered_list_of_primes?(fs2)    
                                                   IMPLIES fs1 = fs2


END unique_factorization