theorem SH1: :: DBLSEQ_2:45

for X being non empty set
for s being sequence of X
for n being Nat holds dom (Shift ((s | (Segm n)),1)) = Seg n