consider psi being Ordinal-Sequence such that

A1: ( dom psi = On F_{1}() & ( for A being Ordinal st A in On F_{1}() holds

psi . A = F_{2}(A) ) )
from ORDINAL2:sch 3();

rng psi c= On F_{1}()
_{1}() by A1, FUNCT_2:def 1, RELSET_1:4;

take psi ; :: thesis: for a being Ordinal of F_{1}() holds psi . a = F_{2}(a)

let a be Ordinal of F_{1}(); :: thesis: psi . a = F_{2}(a)

a in On F_{1}()
by ORDINAL1:def 9;

hence psi . a = F_{2}(a)
by A1; :: thesis: verum

A1: ( dom psi = On F

psi . A = F

rng psi c= On F

proof

then reconsider psi = psi as Ordinal-Sequence of F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng psi or x in On F_{1}() )

assume x in rng psi ; :: thesis: x in On F_{1}()

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_{2}(y)
by A1, A2, A3;

hence x in On F_{1}()
by ORDINAL1:def 9; :: thesis: verum

end;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

hence x in On F

take psi ; :: thesis: for a being Ordinal of F

let a be Ordinal of F

a in On F

hence psi . a = F