consider L being Sequence such that
A1: ( dom L = succ F1() & ( 0 in succ F1() implies L . 0 = F2() ) & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) from ORDINAL2:sch 5();
 thus ex x being object ex L being Sequence st
( x = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) :: thesis: for x1, x2 being set st ex L being Sequence st
( x1 = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being Sequence st
( x2 = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) holds
x1 = x2
proof
take x = last L; :: thesis: ex L being Sequence st
( x = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
take L ; :: thesis: ( x = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
thus ( x = last L & dom L = succ F1() ) by A1; :: thesis: ( L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
0 c= succ F1() ;
then 0 c< succ F1() ;
hence ( L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(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 F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being Sequence st
( x2 = last L & dom L = succ F1() & L . 0 = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) implies x1 = x2 )
given L1 being Sequence such that A2: x1 = 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 L being Sequence holds
( not x2 = last L or not dom L = succ F1() or not L . 0 = F2() or ex C being Ordinal st
( succ C in succ F1() & not L . (succ C) = F3(C,(L . C)) ) or ex C being Ordinal st
( C in succ F1() & C <> 0 & C is limit_ordinal & not L . C = F4(C,(L | C)) ) ) or x1 = x2 )
A7: ( 0 in succ F1() implies L1 . 0 = F2() ) by A4;
given L2 being Sequence such that A8: x2 = last L2 and
A9: dom L2 = succ F1() and
A10: L2 . 0 = F2() and
A11: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = F3(C,(L2 . C)) and
A12: for C being Ordinal st C in succ F1() & C <> 0 & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) ; :: thesis: x1 = x2
A13: ( 0 in succ F1() implies L2 . 0 = F2() ) by A10;
L1 = L2 from ORDINAL2:sch 4(A3, A7, A5, A6, A9, A13, A11, A12);
 hence x1 = x2 by A2, A8; :: thesis: verum