theorem Th20: :: CGAMES_1:20

for f being FinSequence
for n being Nat st n in dom f & n > 1 holds
n - 1 in dom f