theorem Th3: :: SURREAL0:3

for L being Sequence
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