dom (Shift ((s | (Segm n)),1)) = Seg n by SH1;
hence Shift ((s | (Segm n)),1) is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum