consider L being Sequence such that
A1: ( dom L = F₁() & ( for A being Ordinal st A in F₁() holds
L . A = F₂(A) ) ) from ORDINAL2:sch 2();
L is Ordinal-yielding

proof

take sup (rng L) ; :: according to ORDINAL2:def 4 :: thesis: rng L c= sup (rng L)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng L or x in sup (rng L) )
assume A2: x in rng L ; :: thesis: x in sup (rng L)
then consider y being object such that
A3: y in dom L and
A4: x = L . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A3;
L . y = F₂(y) by A1, A3;
then A5: x in On (rng L) by A2, A4, ORDINAL1:def 9;
On (rng L) c= sup (rng L) by Def3;
hence x in sup (rng L) by A5; :: thesis: verum

end;

then reconsider L = L as Ordinal-Sequence ;
take fi = L; :: thesis: ( dom fi = F₁() & ( for A being Ordinal st A in F₁() holds
fi . A = F₂(A) ) )
thus dom fi = F₁() by A1; :: thesis: for A being Ordinal st A in F₁() holds
fi . A = F₂(A)
let A be Ordinal; :: thesis: ( A in F₁() implies fi . A = F₂(A) )
assume A in F₁() ; :: thesis: fi . A = F₂(A)
hence fi . A = F₂(A) by A1; :: thesis: verum