for k, n being Element of NAT st n > 1 & k <> 0 & k <> 1 holds
( Fib k = Fib n iff k = n )