consider fi being Ordinal-Sequence such that
A1: ( dom fi = succ F₁() & ( {} in succ F₁() implies fi . {} = 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 <> {} & 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 . {} = 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 <> {} & 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 . {} = 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 <> {} & 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 . {} = 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 <> {} & 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 . {} = 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 <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) )
take fi ; :: thesis: ( A = last fi & dom fi = succ F₁() & fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) )
thus ( A = last fi & dom fi = succ F₁() ) by A1; :: thesis: ( fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) )
( succ F₁() <> {} & {} c= succ F₁() ) ;
then {} c< succ F₁() by XBOOLE_0:def 8;
hence ( fi . {} = 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 <> {} & C is limit_ordinal holds
fi . C = F₄(C,(fi | C)) ) ) by A1, ORDINAL1:21; :: thesis: verum

end;

let A1, A2 be Ordinal; :: thesis: ( ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F₁() & fi . {} = 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 <> {} & 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 . {} = 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 <> {} & 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 . {} = 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 <> {} & 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 . {} = 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 <> {} & C is limit_ordinal & not fi . C = F₄(C,(fi | C)) ) ) or A1 = A2 )
given L2 being Ordinal-Sequence such that A7: A2 = last L2 and
A8: dom L2 = succ F₁() and
A9: L2 . {} = F₂() and
A10: for C being Ordinal st succ C in succ F₁() holds
L2 . (succ C) = F₃(C,(L2 . C)) and
A11: for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L2 . C = F₄(C,(L2 | C)) ; :: thesis: A1 = A2
A12: ( {} in succ F₁() implies L1 . {} = F₂() ) by A4;
A13: ( {} in succ F₁() implies L2 . {} = F₂() ) by A9;
deffunc H₁( Ordinal, Ordinal) -> Ordinal = F₃($1,(sup (union {$2})));
A14: 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 A15: succ C in succ F₁() ; :: thesis: L1 . (succ C) = H₁(C,L1 . C)
reconsider x' = L1 . C as Ordinal ;
sup (union {(L1 . C)}) = sup x' by ZFMISC_1:31
.= x' by Th26 ;
hence L1 . (succ C) = H₁(C,L1 . C) by A5, A15; :: thesis: verum

end;

A16: 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 A17: succ C in succ F₁() ; :: thesis: L2 . (succ C) = H₁(C,L2 . C)
reconsider x' = L2 . C as Ordinal ;
sup (union {(L2 . C)}) = sup x' by ZFMISC_1:31
.= x' by Th26 ;
hence L2 . (succ C) = H₁(C,L2 . C) by A10, A17; :: thesis: verum

end;

A18: for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L1 . C = F₄(C,(L1 | C)) by A6;
A19: for C being Ordinal st C in succ F₁() & C <> {} & C is limit_ordinal holds
L2 . C = F₄(C,(L2 | C)) by A11;
L1 = L2 from ORDINAL2:sch 4(A3, A12, A14, A18, A8, A13, A16, A19);
hence A1 = A2 by A2, A7; :: thesis: verum