consider fi being Ordinal-Sequence such that
A1: ( dom fi = succ F₁() & ( 0 in succ F₁() implies fi . 0 = F₂() ) & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(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 F₁() & fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) :: thesis: for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F₁() & fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F₁() & fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) holds
A1 = A2

proof

take A ; :: thesis: ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F₁() & fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) )
take fi ; :: thesis: ( A = last fi & dom fi = succ F₁() & fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) )
thus ( A = last fi & dom fi = succ F₁() ) by A1; :: thesis: ( fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) )
0 c= succ F₁() ;
then 0 c< succ F₁() ;
hence ( fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) by A1, ORDINAL1:11; :: thesis: verum

end;

deffunc H₁( Ordinal, Ordinal) -> Ordinal = F₃($1,(sup (union {$2})));
let A1, A2 be Ordinal; :: thesis: ( ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F₁() & fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F₁() & fi . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
fi . (succ C) = F₃(C,(fi . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) implies A1 = A2 )
given L1 being Ordinal-Sequence such that A2: A1 = last L1 and
A3: dom L1 = succ F₁() and
A4: L1 . 0 = F₂() and
A5: for C being Ordinal st succ C in succ F₁() holds
L1 . (succ C) = F₃(C,(L1 . C)) and
A6: for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L1 . C = F₄(C,(L1 | C)) ; :: thesis: ( for fi being Ordinal-Sequence holds
( not A2 = last fi or not dom fi = succ F₁() or not fi . 0 = F₂() or ex C being Ordinal st
( succ C in succ F₁() & not fi . (succ C) = F₃(C,(fi . C)) ) or ex C being Ordinal st
( C in succ F₁() & C <> 0 & C is limit_ordinal & not fi . C = F₄(C,(fi | C)) ) ) or A1 = A2 )
A7: ( 0 in succ F₁() implies L1 . 0 = F₂() ) by A4;
A8: for C being Ordinal st succ C in succ F₁() holds
L1 . (succ C) = H₁(C,L1 . C)

proof

let C be Ordinal; :: thesis: ( succ C in succ F₁() implies L1 . (succ C) = H₁(C,L1 . C) )
assume A9: succ C in succ F₁() ; :: thesis: L1 . (succ C) = H₁(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) = H₁(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 F₁() and
A12: L2 . 0 = F₂() and
A13: for C being Ordinal st succ C in succ F₁() holds
L2 . (succ C) = F₃(C,(L2 . C)) and
A14: for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L2 . C = F₄(C,(L2 | C)) ; :: thesis: A1 = A2
A15: for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L2 . C = F₄(C,(L2 | C)) by A14;
A16: for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L1 . C = F₄(C,(L1 | C)) by A6;
A17: for C being Ordinal st succ C in succ F₁() holds
L2 . (succ C) = H₁(C,L2 . C)

proof

let C be Ordinal; :: thesis: ( succ C in succ F₁() implies L2 . (succ C) = H₁(C,L2 . C) )
assume A18: succ C in succ F₁() ; :: thesis: L2 . (succ C) = H₁(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) = H₁(C,L2 . C) by A13, A18; :: thesis: verum

end;

A19: ( 0 in succ F₁() implies L2 . 0 = F₂() ) by A12;
L1 = L2 from ORDINAL2:sch 4(A3, A7, A8, A16, A11, A19, A17, A15);
hence A1 = A2 by A2, A10; :: thesis: verum