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 ) } ;
consider L being Sequence such that
A1: dom L = succ O and
A2: for B being Ordinal
for L1 being Sequence st B in succ O & L1 = L | B holds
L . B = H₁(L1) from ORDINAL1:sch 4();
A3: O in succ O by ORDINAL1:6;
A4: L . O = H₁(L | O) by A2, ORDINAL1:6;
A5: dom (L | O) = O by RELAT_1:62, A3, A1, ORDINAL1:def 2;
L . O c= Games O

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in L . O or y in Games O )
assume y in L . O ; :: thesis: y in Games O
then ex x being Element of Games O st
( y = x & L_ x c= union (rng (L | O)) & R_ x c= union (rng (L | O)) & L_ x << R, R_ x ) by A4, A5;
hence y in Games O ; :: thesis: verum

end;

then reconsider IT = L . O as Subset of (Games O) ;
take IT ; :: thesis: ex L being Sequence st
( IT = 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 ) } ) )
take L ; :: thesis: ( IT = 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 ) } ) )
thus ( IT = L . O & dom L = succ O ) by A1; :: thesis: 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 ) }
let A be Ordinal; :: thesis: ( A in succ O implies 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 ) } )
assume A6: A in succ O ; :: thesis: 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 ) }
A7: dom (L | A) = A by A1, RELAT_1:62, A6, ORDINAL1:def 2;
hence L . A c= { 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 ) } by A2, A6; :: according to XBOOLE_0:def 10 :: thesis: { 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 ) } c= L . A
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { 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 y in L . A )
assume y in { 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 ) } ; :: thesis: y in L . A
hence y in L . A by A7, A2, A6; :: thesis: verum