let O be Ordinal; :: thesis: for R being Relation
for L being Sequence st 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 ) } ) holds
for A being Ordinal st A in succ O holds
L . A = Day (R,A)
let R be Relation; :: thesis: for L being Sequence st 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 ) } ) holds
for A being Ordinal st A in succ O holds
L . A = Day (R,A)
let L be Sequence; :: thesis: ( 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 for A being Ordinal st A in succ O holds
L . A = Day (R,A) )
assume that
A1: dom L = succ O and
A2: 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 ) } ; :: thesis: for A being Ordinal st A in succ O holds
L . A = Day (R,A)
let D be Ordinal; :: thesis: ( D in succ O implies L . D = Day (R,D) )
assume A3: D in succ O ; :: thesis: L . D = Day (R,D)
consider LO being Sequence such that
A4: ( Day (R,D) = LO . D & dom LO = succ D ) and
A5: for A being Ordinal st A in succ D holds
LO . A = { x where x is Element of Games A : ( L_ x c= union (rng (LO | A)) & R_ x c= union (rng (LO | A)) & L_ x << R, R_ x ) } by Def6;
defpred S₁[ Ordinal] means ( $1 c= D 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= D ; :: thesis: LO . A = L . A
then A9: A in succ D by ORDINAL1:22;
A10: A in succ O by A8, A3, ORDINAL1:12;
A11: 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 ) } 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 A8, ORDINAL1:22, A5, A11; :: thesis: verum

end;

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