consider L being Sequence such that
A1:
( Games 0 = L . 0 & dom L = succ 0 )
and
A2:
for O being Ordinal st O in succ 0 holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):]
by Def4;
A3:
L . 0 = [:(bool (union (rng (L | 0)))),(bool (union (rng (L | 0)))):]
by A2, ORDINAL1:6;
bool (union (rng (L | 0))) = {{}}
by ZFMISC_1:1, ZFMISC_1:2;
hence
Games 0 = {[{},{}]}
by A1, A3, ZFMISC_1:29; verum