theorem Th13: :: AFINSQ_1:94

for D being set
for p being FinSequence of D
for n being Nat holds
( n + 1 in dom p iff n in dom (FS2XFS p) )