let L be Sequence; :: thesis: for O being Ordinal st dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] ) holds
for A being Ordinal st A in succ O holds
L . A = Games A
let Ord be Ordinal; :: thesis: ( dom L = succ Ord & ( for A being Ordinal st A in succ Ord holds
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] ) implies for A being Ordinal st A in succ Ord holds
L . A = Games A )
assume that
A1: dom L = succ Ord and
A2: for A being Ordinal st A in succ Ord holds
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] ; :: thesis: for A being Ordinal st A in succ Ord holds
L . A = Games A
let O be Ordinal; :: thesis: ( O in succ Ord implies L . O = Games O )
assume A3: O in succ Ord ; :: thesis: L . O = Games O
consider LO being Sequence such that
A4: ( Games O = LO . O & dom LO = succ O ) and
A5: for A being Ordinal st A in succ O holds
LO . A = [:(bool (union (rng (LO | A)))),(bool (union (rng (LO | A)))):] by Def4;
defpred S₁[ Ordinal] means ( $1 c= O implies LO . $1 = L . $1 );
A6: for A being Ordinal st ( for C being Ordinal st C in A holds
S₁[C] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S₁[C] ) implies S₁[A] )
assume A7: for C being Ordinal st C in A holds
S₁[C] ; :: thesis: S₁[A]
assume A8: A c= O ; :: thesis: LO . A = L . A
then A9: A in succ O by ORDINAL1:22;
A10: A in succ Ord by A8, A3, ORDINAL1:12;
A11: L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] by A2, A8, A3, ORDINAL1:12;
A12: ( dom (L | A) = A & dom (LO | A) = A ) by A4, A1, A9, ORDINAL1:def 2, RELAT_1:62, A10;
for x being object st x in A holds
(LO | A) . x = (L | A) . x

proof

let x be object ; :: thesis: ( x in A implies (LO | A) . x = (L | A) . x )
assume A13: x in A ; :: thesis: (LO | A) . x = (L | A) . x
reconsider x = x as Ordinal by A13;
(LO | A) . x = LO . x by A13, FUNCT_1:49
.= L . x by A13, A7, A8, ORDINAL1:def 2 ;
hence (LO | A) . x = (L | A) . x by A13, FUNCT_1:49; :: thesis: verum

end;

then LO | A = L | A by A12, FUNCT_1:2;
hence LO . A = L . A by A5, A8, ORDINAL1:22, A11; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A6);
hence L . O = Games O by A4; :: thesis: verum