consider L being Sequence such that
A1: ( dom L = succ F₁() & ( 0 in succ F₁() implies L . 0 = F₂() ) & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) from ORDINAL2:sch 5();
thus ex x being object ex L being Sequence st
( x = last L & dom L = succ F₁() & L . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) :: thesis: for x1, x2 being set st ex L being Sequence st
( x1 = last L & dom L = succ F₁() & L . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) & ex L being Sequence st
( x2 = last L & dom L = succ F₁() & L . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) holds
x1 = x2

proof

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

end;

let x1, x2 be set ; :: thesis: ( ex L being Sequence st
( x1 = last L & dom L = succ F₁() & L . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) & ex L being Sequence st
( x2 = last L & dom L = succ F₁() & L . 0 = F₂() & ( for C being Ordinal st succ C in succ F₁() holds
L . (succ C) = F₃(C,(L . C)) ) & ( for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L . C = F₄(C,(L | C)) ) ) implies x1 = x2 )
given L1 being Sequence such that A2: x1 = 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 L being Sequence holds
( not x2 = last L or not dom L = succ F₁() or not L . 0 = F₂() or ex C being Ordinal st
( succ C in succ F₁() & not L . (succ C) = F₃(C,(L . C)) ) or ex C being Ordinal st
( C in succ F₁() & C <> 0 & C is limit_ordinal & not L . C = F₄(C,(L | C)) ) ) or x1 = x2 )
A7: ( 0 in succ F₁() implies L1 . 0 = F₂() ) by A4;
given L2 being Sequence such that A8: x2 = last L2 and
A9: dom L2 = succ F₁() and
A10: L2 . 0 = F₂() and
A11: for C being Ordinal st succ C in succ F₁() holds
L2 . (succ C) = F₃(C,(L2 . C)) and
A12: for C being Ordinal st C in succ F₁() & C <> 0 & C is limit_ordinal holds
L2 . C = F₄(C,(L2 | C)) ; :: thesis: x1 = x2
A13: ( 0 in succ F₁() implies L2 . 0 = F₂() ) by A10;
L1 = L2 from ORDINAL2:sch 4(A3, A7, A5, A6, A9, A13, A11, A12);
hence x1 = x2 by A2, A8; :: thesis: verum