let s be FinSequence; :: thesis: ( 1 <= len s implies len (Op-LeftShift s) = len s )
assume A1: 1 <= len s ; :: thesis: len (Op-LeftShift s) = len s
A2: len <*(s . 1)*> = 1 by FINSEQ_1:40;
len (s /^ 1) = (len s) - 1 by A1, RFINSEQ:def 1;
then len ((s /^ 1) ^ <*(s . 1)*>) = ((len s) - 1) + 1 by A2, FINSEQ_1:22
.= len s ;
hence len (Op-LeftShift s) = len s ; :: thesis: verum