let k, n be Element of NAT ; :: thesis: ( n > 1 & k <> 0 & k <> 1 implies ( Fib k = Fib n iff k = n ) )
assume that
A1: n > 1 and
A2: ( k <> 0 & k <> 1 ) ; :: thesis: ( Fib k = Fib n iff k = n )
not k is trivial by A2, NAT_2:def 1;
then k >= 1 + 1 by NAT_2:29;
then A3: k > 1 by NAT_1:13;
( Fib k = Fib n implies k = n )

proof

assume A4: Fib k = Fib n ; :: thesis: k = n
assume A5: k <> n ; :: thesis: contradiction

per cases ( k > n or k < n ) by A5, XXREAL_0:1;

suppose k > n ; :: thesis: contradiction

hence contradiction by A1, A4, Th46; :: thesis: verum

end;

suppose k < n ; :: thesis: contradiction

hence contradiction by A3, A4, Th46; :: thesis: verum

end;

end;

end;

hence ( Fib k = Fib n iff k = n ) ; :: thesis: verum