let x be set ; :: according to CGAMES_1:def 10 :: thesis: ( x in dom <*g*> implies <*g*> . x is ConwayGame )
assume x in dom <*g*> ; :: thesis: <*g*> . x is ConwayGame
then x = 1 by FINSEQ_1:90;
hence <*g*> . x is ConwayGame by FINSEQ_1:def 8; :: thesis: verum