:: deftheorem defines Fibonacci_inv_pred NOMIN_7:def 18 :
for V, A being set
for loc being b₁ -valued Function
for n0 being Nat
for d being object holds
( Fibonacci_inv_pred A,loc,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6)} c= dom d1 & d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = n0 & ex I being Nat st
( I = d1 . (loc /. 1) & d1 . (loc /. 4) = Fib I & d1 . (loc /. 5) = Fib (I + 1) ) ) );