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

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A5: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
assume A6: D c= A ; :: thesis: La . D = Lb . D
B c= succ B by XBOOLE_1:7;
then ( A c= succ A & A c= succ B ) by XBOOLE_1:7, A1, XBOOLE_1:1;
then A7: ( dom (La | D) = D & D = dom (Lb | D) ) by A2, A3, RELAT_1:62, A6, XBOOLE_1:1;
for x being object st x in D holds
(La | D) . x = (Lb | D) . x

proof

let x be object ; :: thesis: ( x in D implies (La | D) . x = (Lb | D) . x )
assume A8: x in D ; :: thesis: (La | D) . x = (Lb | D) . x
reconsider o = x as Ordinal by A8;
thus (La | D) . x = La . o by A8, FUNCT_1:49
.= Lb . o by A8, ORDINAL1:def 2, A6, A5
.= (Lb | D) . x by A8, FUNCT_1:49 ; :: thesis: verum

end;

then A9: La | D = Lb | D by A7, FUNCT_1:2;
A10: ( D c= B & B in succ B ) by A1, A6, ORDINAL1:6, XBOOLE_1:1;
D in succ A by ORDINAL1:6, A6, ORDINAL1:12;
hence La . D = [:(bool (union (rng (Lb | D)))),(bool (union (rng (Lb | D)))):] by A2, A9
.= Lb . D by A10, A3, ORDINAL1:12 ;
:: thesis: verum

end;

A11: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A4);
A12: Lb . B = [:(bool (union (rng (Lb | B)))),(bool (union (rng (Lb | B)))):] by A3, ORDINAL1:6;
A13: La . A = [:(bool (union (rng (La | A)))),(bool (union (rng (La | A)))):] by ORDINAL1:6, A2;
rng (La | A) c= rng (Lb | B)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (La | A) or y in rng (Lb | B) )
assume A14: y in rng (La | A) ; :: thesis: y in rng (Lb | B)
consider x being object such that
A15: ( x in dom (La | A) & (La | A) . x = y ) by A14, FUNCT_1:def 3;
A16: ( dom (La | A) = A & dom (Lb | B) = B ) by A2, A3, RELAT_1:62, XBOOLE_1:7;
reconsider x = x as Ordinal by A15;
(La | A) . x = La . x by A15, FUNCT_1:49
.= Lb . x by A15, ORDINAL1:def 2, A11
.= (Lb | B) . x by A1, A15, A16, FUNCT_1:49 ;
hence y in rng (Lb | B) by A1, A16, A15, FUNCT_1:def 3; :: thesis: verum

end;

then union (rng (La | A)) c= union (rng (Lb | B)) by ZFMISC_1:77;
then bool (union (rng (La | A))) c= bool (union (rng (Lb | B))) by ZFMISC_1:67;
hence Games A c= Games B by A2, A3, A12, A13, ZFMISC_1:96; :: thesis: verum