let X be non empty set ; :: thesis: for s being sequence of X
for n being Nat holds Shift ((s | (Segm n)),1) is FinSequence of X
let s be sequence of X; :: thesis: for n being Nat holds Shift ((s | (Segm n)),1) is FinSequence of X
let n be Nat; :: thesis: Shift ((s | (Segm n)),1) is FinSequence of X
rng (Shift ((s | (Segm n)),1)) c= X ;
hence Shift ((s | (Segm n)),1) is FinSequence of X by FINSEQ_1:def 4; :: thesis: verum