consider L being T-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 A = sup (rng L); :: according to ORDINAL2:def 8 :: thesis: rng L c= A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng L or x in A )
assume A2: x in rng L ; :: thesis: x in A
then consider y being set such that
A3: ( y in dom L & x = L . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A3;
L . y = F₂(y) by A1, A3;
then ( x in On (rng L) & On (rng L) c= sup (rng L) ) by A2, A3, Def7, ORDINAL1:def 10;
hence x in A ; :: 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