consider psi being Ordinal-Sequence such that
A1: ( dom psi = On F₁() & ( for A being Ordinal st A in On F₁() holds
psi . A = F₂(A) ) ) from ORDINAL2:sch 3();
rng psi c= On F₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng psi or x in On F₁() )
assume x in rng psi ; :: thesis: x in On F₁()
then consider y being set such that
A2: ( y in dom psi & x = psi . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A2;
( x = F₂(y) & F₂(y) in F₁() ) by A1, A2;
hence x in On F₁() by ORDINAL1:def 10; :: thesis: verum

end;

then reconsider psi = psi as Ordinal-Sequence of F₁() by A1, FUNCT_2:def 1, RELSET_1:11;
take psi ; :: thesis: for a being Ordinal of F₁() holds psi . a = F₂(a)
let a be Ordinal of F₁(); :: thesis: psi . a = F₂(a)
a in On F₁() by ORDINAL1:def 10;
hence psi . a = F₂(a) by A1; :: thesis: verum