for B being Ordinal st B in dom F₁() holds
F₁() . B = F₃((F₁() | B))

A1: for A being Ordinal
for a being object holds
( a = F₂(A) iff ex L being Sequence st
( a = F₃(L) & dom L = A & ( for B being Ordinal st B in A holds
L . B = F₃((L | B)) ) ) ) and
A2: for A being Ordinal st A in dom F₁() holds
F₁() . A = F₂(A)