ex k being Nat st
( F₁(k) = 0 & ( for n being Nat st F₁(n) = 0 holds
k <= n ) )

A1: for k being Nat holds
( F₁((k + 1)) < F₁(k) or F₁(k) = 0 )