deffunc H1( Ordinal, set ) -> object = [{$2},{}];
deffunc H2( Ordinal, Sequence) -> object = [(rng $2),{}];
let IT1, IT2 be set ; ( ex S being Sequence st
( IT1 = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) & ex S being Sequence st
( IT2 = S . A & dom S = succ A & ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) implies IT1 = IT2 )
given S1 being Sequence such that A7:
IT1 = S1 . A
and
A8:
dom S1 = succ A
and
A9:
for O being Ordinal st succ O in succ A holds
S1 . (succ O) = H1(O,S1 . O)
and
A10:
for O being Ordinal st O in succ A & O is limit_ordinal holds
S1 . O = H2(O,S1 | O)
; ( for S being Sequence holds
( not IT2 = S . A or not dom S = succ A or ex O being Ordinal st
( succ O in succ A & not S . (succ O) = [{(S . O)},{}] ) or ex O being Ordinal st
( O in succ A & O is limit_ordinal & not S . O = [(rng (S | O)),{}] ) ) or IT1 = IT2 )
given S2 being Sequence such that A11:
IT2 = S2 . A
and
A12:
dom S2 = succ A
and
A13:
for O being Ordinal st succ O in succ A holds
S2 . (succ O) = H1(O,S2 . O)
and
A14:
for O being Ordinal st O in succ A & O is limit_ordinal holds
S2 . O = H2(O,S2 | O)
; IT1 = IT2
0 c= A
;
then A15:
( S1 . 0 = H2( 0 ,S1 | 0) & H2( 0 ,S2 | 0) = S2 . 0 )
by ORDINAL1:22, ORDINAL2:4, A10, A14;
A16:
( 0 in succ A implies S1 . 0 = 0_No )
by A15;
A17:
( 0 in succ A implies S2 . 0 = 0_No )
by A15;
A18:
for O being Ordinal st O in succ A & O <> 0 & O is limit_ordinal holds
S1 . O = H2(O,S1 | O)
by A10;
A19:
for O being Ordinal st O in succ A & O <> 0 & O is limit_ordinal holds
S2 . O = H2(O,S2 | O)
by A14;
S1 = S2
from ORDINAL2:sch 4(A8, A16, A9, A18, A12, A17, A13, A19);
hence
IT1 = IT2
by A7, A11; verum