for A being Ordinal st A in dom F₁() holds
F₁() . A = F₂(A)

A1: for A being Ordinal
for x being object holds
( x = F₂(A) iff ex L being Sequence st
( x = last L & dom L = succ A & L . 0 = F₄() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F₅(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> 0 & C is limit_ordinal holds
L . C = F₆(C,(L | C)) ) ) ) and
A2: dom F₁() = F₃() and
A3: ( 0 in F₃() implies F₁() . 0 = F₄() ) and
A4: for A being Ordinal st succ A in F₃() holds
F₁() . (succ A) = F₅(A,(F₁() . A)) and
A5: for A being Ordinal st A in F₃() & A <> 0 & A is limit_ordinal holds
F₁() . A = F₆(A,(F₁() | A))