  The original F5 algorithm introduced by Faug\`ere is formulated for any
homogeneous polynomial set input. The correctness of output is shown for any
input that terminates the algorithm, but the termination itself is proved only
for the case of input being regular polynomial sequence. This article shows
that algorithm correctly terminates for any homogeneous input without any
reference to regularity. The scheme contains two steps: first it is shown that
if the algorithm does not terminate it eventually generates two polynomials
where first is a reductor for the second. But first step does not show that
this reduction is permitted by criteria introduced in F5. The second step shows
that if such pair exists then there exists another pair for which the reduction
is permitted by all criteria. Existence of such pair leads to contradiction.
  Version v3 fixes the bibliography.
