consider fi being Ordinal-Sequence such that
A1: ( dom fi = succ F1() & ( 0 in succ F1() implies fi . 0 = F2() ) & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) from ORDINAL2:sch 11();
 reconsider A = last fi as Ordinal ;
thus ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) :: thesis: for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) holds
A1 = A2
proof
take A ; :: thesis: ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
take fi ; :: thesis: ( A = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
thus ( A = last fi & dom fi = succ F1() ) by A1; :: thesis: ( fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
0 c= succ F1() ;
then 0 c< succ F1() ;
hence ( fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) by A1, ORDINAL1:11; :: thesis: verum
end;
deffunc H1( Ordinal, Ordinal) -> Ordinal = F3($1,(sup (union {$2})));
let A1, A2 be Ordinal; :: thesis: ( ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) implies A1 = A2 )
given L1 being Ordinal-Sequence such that A2: A1 = last L1 and
A3: dom L1 = succ F1() and
A4: L1 . 0 = F2() and
A5: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = F3(C,(L1 . C)) and
A6: for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) ; :: thesis: ( for fi being Ordinal-Sequence holds
( not A2 = last fi or not dom fi = succ F1() or not fi . 0 = F2() or ex C being Ordinal st
( succ C in succ F1() & not fi . (succ C) = F3(C,(fi . C)) ) or ex C being Ordinal st
( C in succ F1() & C <> 0 & C is limit_ordinal & not fi . C = F4(C,(fi | C)) ) ) or A1 = A2 )
A7: ( 0 in succ F1() implies L1 . 0 = F2() ) by A4;
A8: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = H1(C,L1 . C)
proof
let C be Ordinal; :: thesis: ( succ C in succ F1() implies L1 . (succ C) = H1(C,L1 . C) )
assume A9: succ C in succ F1() ; :: thesis: L1 . (succ C) = H1(C,L1 . C)
reconsider x9 = L1 . C as Ordinal ;
sup (union {(L1 . C)}) = sup x9 by ZFMISC_1:25
.= x9 by Th18 ;
hence L1 . (succ C) = H1(C,L1 . C) by A5, A9; :: thesis: verum
end;
given L2 being Ordinal-Sequence such that A10: A2 = last L2 and
A11: dom L2 = succ F1() and
A12: L2 . 0 = F2() and
A13: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = F3(C,(L2 . C)) and
A14: for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) ; :: thesis: A1 = A2
A15: for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) by A14;
A16: for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) by A6;
A17: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = H1(C,L2 . C)
proof
let C be Ordinal; :: thesis: ( succ C in succ F1() implies L2 . (succ C) = H1(C,L2 . C) )
assume A18: succ C in succ F1() ; :: thesis: L2 . (succ C) = H1(C,L2 . C)
reconsider x9 = L2 . C as Ordinal ;
sup (union {(L2 . C)}) = sup x9 by ZFMISC_1:25
.= x9 by Th18 ;
hence L2 . (succ C) = H1(C,L2 . C) by A13, A18; :: thesis: verum
end;
A19: ( 0 in succ F1() implies L2 . 0 = F2() ) by A12;
L1 = L2 from ORDINAL2:sch 4(A3, A7, A8, A16, A11, A19, A17, A15);
 hence A1 = A2 by A2, A10; :: thesis: verum