F₁() is finite

A1: F₂((F₁() . 0)) is finite and
A2: for a being Ordinal st succ a in dom F₁() & F₂((F₁() . a)) is finite holds
F₂((F₁() . (succ a))) c< F₂((F₁() . a))