theorem SH2: :: DBLSEQ_2:46

for X being non empty set
for s being sequence of X
for n being Nat holds Shift ((s | (Segm n)),1) is FinSequence of X