theorem Th1: :: NUMBER15:1

for n being Nat
for f being XFinSequence st n in dom (XFS2FS f) holds
n - 1 in dom f