:: deftheorem defines Fib PRE_FF:def 2 :
for n being Nat holds Fib n = (Fib . n) `1 ;