theorem :: NUMBER16:14

( ( for i, j being Nat st 0 < i & i <= 7 holds
ex k being Nat st (ArProg (j,i)) . k is Fibonacci ) & ( for k being Nat holds not (ArProg (4,8)) . k is Fibonacci ) )