deffunc H1( Ordinal, set ) -> Ordinal = F3($1,(sup (union {$2})));
consider L being Sequence such that
A1: dom L = F1() and
A2: ( 0 in F1() implies L . 0 = F2() ) and
A3: for A being Ordinal st succ A in F1() holds
L . (succ A) = H1(A,L . A) and
A4: for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
L . A = F4(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 = F4(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 = F3(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 = F1() & ( 0 in F1() implies fi . 0 = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
thus ( dom fi = F1() & ( 0 in F1() implies fi . 0 = F2() ) ) by A1, A2; :: thesis: ( ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
thus for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) :: thesis: for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
fi . A = F4(A,(fi | A))
proof
let A be Ordinal; :: thesis: ( succ A in F1() implies fi . (succ A) = F3(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 F1() implies fi . (succ A) = F3(A,(fi . A)) ) by A3; :: thesis: verum
end;
thus for A being Ordinal st A in F1() & A <> 0 & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) by A4; :: thesis: verum