deffunc H₁( Ordinal, set ) -> Ordinal = F₃($1,(sup (union {$2})));
consider L being Sequence such that
A1: dom L = F₁() and
A2: ( 0 in F₁() implies L . 0 = 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 <> 0 & A is limit_ordinal holds
L . A = F₄(A,(L | A)) from ORDINAL2:sch 5();
L is Ordinal-yielding

proof

take sup (rng L) ; :: according to ORDINAL2:def 4 :: thesis: rng L c= sup (rng L)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng L or x in sup (rng L) )
assume A5: x in rng L ; :: thesis: x in sup (rng L)
then consider y being object such that
A6: y in dom L and
A7: x = L . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A6;

A8: now :: thesis: ( y <> 0 & ( for B being Ordinal holds y <> succ B ) implies x is Ordinal )

assume that
A9: y <> 0 and
A10: for B being Ordinal holds y <> succ B ; :: thesis: x is Ordinal
y is limit_ordinal by A10, ORDINAL1:29;
then L . y = F₄(y,(L | y)) by A1, A4, A6, A9;
hence x is Ordinal by A7; :: thesis: verum

end;

A11: On (rng L) c= sup (rng L) by Def3;

now :: thesis: ( ex B being Ordinal st y = succ B implies x is Ordinal )

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

end;

then x in On (rng L) by A1, A2, A5, A6, A7, A8, ORDINAL1:def 9;
hence x in sup (rng L) by A11; :: thesis: verum

end;

then reconsider L = L as Ordinal-Sequence ;
take fi = L; :: thesis: ( dom fi = F₁() & ( 0 in F₁() implies fi . 0 = 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 <> 0 & A is limit_ordinal holds
fi . A = F₄(A,(fi | A)) ) )
thus ( dom fi = F₁() & ( 0 in F₁() implies fi . 0 = 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 <> 0 & 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 <> 0 & 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:25
.= B by Th18 ;
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 <> 0 & A is limit_ordinal holds
fi . A = F₄(A,(fi | A)) by A4; :: thesis: verum