:: deftheorem defines valid_Fibonacci_output_pred NOMIN_7:def 16 :
for V, A being set
for z being Element of V
for n0 being Nat
for d being object holds
( valid_Fibonacci_output_pred A,z,n0,d iff ex d1 being NonatomicND of V,A st
( d = d1 & z in dom d1 & d1 . z = Fib n0 ) );