let n be Element of dom <*g*>; :: according to CGAMES_1:def 11 :: thesis: ( n > 1 implies <*g*> . (n - 1) in the_Options_of (<*g*> . n) )
dom <*g*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
hence ( n > 1 implies <*g*> . (n - 1) in the_Options_of (<*g*> . n) ) by TARSKI:def 1; :: thesis: verum