let D be non empty set ; :: thesis: for s being FinSequence of D st 1 <= len s holds
Op-RightShift s is FinSequence of D
let s be FinSequence of D; :: thesis: ( 1 <= len s implies Op-RightShift s is FinSequence of D )
assume 1 <= len s ; :: thesis: Op-RightShift s is FinSequence of D
then len s in Seg (len s) ;
then len s in dom s by FINSEQ_1:def 3;
then s . (len s) is Element of D by FINSEQ_2:11;
then <*(s . (len s))*> is FinSequence of D by FINSEQ_1:74;
then reconsider ss = <*(s . (len s))*> ^ s as FinSequence of D by FINSEQ_1:75;
ss | (len s) is FinSequence of D ;
hence Op-RightShift s is FinSequence of D ; :: thesis: verum