let X1, X2 be Subset of (Games O); :: thesis: ( ex L being Sequence st
( X1 = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) ) & ex L being Sequence st
( X2 = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) ) implies X1 = X2 )
given L1 being Sequence such that A8: ( X1 = L1 . O & dom L1 = succ O ) and
A9: for A being Ordinal st A in succ O holds
L1 . A = { x where x is Element of Games A : ( L_ x c= union (rng (L1 | A)) & R_ x c= union (rng (L1 | A)) & L_ x << R, R_ x ) } ; :: thesis: ( for L being Sequence holds
( not X2 = L . O or not dom L = succ O or ex A being Ordinal st
( A in succ O & not L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) ) or X1 = X2 )
given L2 being Sequence such that A10: ( X2 = L2 . O & dom L2 = succ O ) and
A11: for A being Ordinal st A in succ O holds
L2 . A = { x where x is Element of Games A : ( L_ x c= union (rng (L2 | A)) & R_ x c= union (rng (L2 | A)) & L_ x << R, R_ x ) } ; :: thesis: X1 = X2
deffunc H₁( Sequence) -> set = { x where x is Element of Games (dom $1) : ( L_ x c= union (rng $1) & R_ x c= union (rng $1) & L_ x << R, R_ x ) } ;
A12: ( dom L1 = succ O & ( for B being Ordinal
for L being Sequence st B in succ O & L = L1 | B holds
L1 . B = H₁(L) ) )

proof

thus dom L1 = succ O by A8; :: thesis: for B being Ordinal
for L being Sequence st B in succ O & L = L1 | B holds
L1 . B = H₁(L)
let B be Ordinal; :: thesis: for L being Sequence st B in succ O & L = L1 | B holds
L1 . B = H₁(L)
let L be Sequence; :: thesis: ( B in succ O & L = L1 | B implies L1 . B = H₁(L) )
assume A13: ( B in succ O & L = L1 | B ) ; :: thesis: L1 . B = H₁(L)
A14: dom (L1 | B) = B by A13, A8, RELAT_1:62, ORDINAL1:def 2;
thus L1 . B c= H₁(L) by A14, A13, A9; :: according to XBOOLE_0:def 10 :: thesis: H₁(L) c= L1 . B
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H₁(L) or y in L1 . B )
thus ( not y in H₁(L) or y in L1 . B ) by A13, A14, A9; :: thesis: verum

end;

A15: ( dom L2 = succ O & ( for B being Ordinal
for L being Sequence st B in succ O & L = L2 | B holds
L2 . B = H₁(L) ) )

proof

thus dom L2 = succ O by A10; :: thesis: for B being Ordinal
for L being Sequence st B in succ O & L = L2 | B holds
L2 . B = H₁(L)
let B be Ordinal; :: thesis: for L being Sequence st B in succ O & L = L2 | B holds
L2 . B = H₁(L)
let L be Sequence; :: thesis: ( B in succ O & L = L2 | B implies L2 . B = H₁(L) )
assume A16: ( B in succ O & L = L2 | B ) ; :: thesis: L2 . B = H₁(L)
dom (L2 | B) = B by A16, A10, RELAT_1:62, ORDINAL1:def 2;
hence L2 . B = H₁(L) by A16, A11; :: thesis: verum

end;

L1 = L2 from ORDINAL1:sch 3(A12, A15);
hence X1 = X2 by A8, A10; :: thesis: verum