deffunc H₁( Ordinal, set ) -> Ordinal = F₃($1,(sup (union {$2})));
consider L being T-Sequence such that
A1: dom L = F₁() and
A2: ( {} in F₁() implies L . {} = F₂() ) and
A3: for A being Ordinal st succ A in F₁() holds
L . (succ A) = H₁(A,L . A) and
A4: for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
L . A = F₄(A,(L | A)) from ORDINAL2:sch 5();
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 A5: x in rng L ; :: thesis: x in A
then consider y being set such that
A6: ( y in dom L & x = L . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A6;

A7: now

given B being Ordinal such that A8: y = succ B ; :: thesis: x is Ordinal
L . y = F₃(B,(sup (union {(L . B)}))) by A1, A3, A6, A8;
hence x is Ordinal by A6; :: thesis: verum

end;

now

assume A9: ( y <> {} & ( for B being Ordinal holds y <> succ B ) ) ; :: thesis: x is Ordinal
then y is limit_ordinal by ORDINAL1:42;
then L . y = F₄(y,(L | y)) by A1, A4, A6, A9;
hence x is Ordinal by A6; :: thesis: verum

end;

then ( x in On (rng L) & On (rng L) c= sup (rng L) ) by A1, A2, A5, A6, A7, 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₁() & ( {} in F₁() implies fi . {} = F₂() ) & ( for A being Ordinal st succ A in F₁() holds
fi . (succ A) = F₃(A,(fi . A)) ) & ( for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
fi . A = F₄(A,(fi | A)) ) )
thus ( dom fi = F₁() & ( {} in F₁() implies fi . {} = F₂() ) ) by A1, A2; :: thesis: ( ( for A being Ordinal st succ A in F₁() holds
fi . (succ A) = F₃(A,(fi . A)) ) & ( for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
fi . A = F₄(A,(fi | A)) ) )
thus for A being Ordinal st succ A in F₁() holds
fi . (succ A) = F₃(A,(fi . A)) :: thesis: for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
fi . A = F₄(A,(fi | A))

proof

let A be Ordinal; :: thesis: ( succ A in F₁() implies fi . (succ A) = F₃(A,(fi . A)) )
reconsider B = fi . A as Ordinal ;
sup (union {B}) = sup B by ZFMISC_1:31
.= B by Th26 ;
hence ( succ A in F₁() implies fi . (succ A) = F₃(A,(fi . A)) ) by A3; :: thesis: verum

end;

thus for A being Ordinal st A in F₁() & A <> {} & A is limit_ordinal holds
fi . A = F₄(A,(fi | A)) by A4; :: thesis: verum