theorem SH4: :: DBLSEQ_2:48

for X being non empty set
for s being sequence of X holds
( Shift ((s | (Segm 0)),1) = {} & Shift ((s | (Segm 1)),1) = <*(s . 0)*> & Shift ((s | (Segm 2)),1) = <*(s . 0),(s . 1)*> & ( for n being Nat holds Shift ((s | (Segm (n + 1))),1) = (Shift ((s | (Segm n)),1)) ^ <*(s . n)*> ) )