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 & len (Op-RightShift s) = len s )
let s be FinSequence of D; :: thesis: ( 1 <= len s implies ( Op-RightShift s is FinSequence of D & len (Op-RightShift s) = len s ) )
assume 1 <= len s ; :: thesis: ( Op-RightShift s is FinSequence of D & len (Op-RightShift s) = len s )
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 & len (Op-RightShift s) = len s ) by LM004; :: thesis: verum