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 object ; :: 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 object such that
A2: y in dom psi and
A3: x = psi . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A2;
x = F₂(y) by A1, A2, A3;
hence x in On F₁() by ORDINAL1:def 9; :: thesis: verum

end;

then reconsider psi = psi as Ordinal-Sequence of F₁() by A1, FUNCT_2:def 1, RELSET_1:4;
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 9;
hence psi . a = F₂(a) by A1; :: thesis: verum