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