theorem SH3: :: DBLSEQ_2:47

for X being non empty set
for s being sequence of X
for n, m being Nat st m + 1 in dom (Shift ((s | (Segm n)),1)) holds
(Shift ((s | (Segm n)),1)) . (m + 1) = s . m