( F₁() c= Union F₂() & F₃((Union F₂())) = Union F₂() & ( for b being Ordinal st F₁() c= b & F₃(b) = b holds
Union F₂() c= b ) )

A1: for a, b being Ordinal st a in b holds
F₃(a) in F₃(b) and
A2: for a being Ordinal st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = F₃(b) ) holds
F₃(a) is_limes_of phi and
A3: ( dom F₂() = omega & F₂() . 0 = F₁() ) and
A4: for a being Ordinal st a in omega holds
F₂() . (succ a) = F₃((F₂() . a))