let m, n be Nat; :: thesis: ( Fermat m = Fermat n implies m = n )
assume Fermat m = Fermat n ; :: thesis: m = n
then 2 |^ m = 2 |^ n by PEPIN:30;
hence m = n by PEPIN:30; :: thesis: verum