let D be non empty set ; :: thesis: for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,1) = Op-LeftShift s
let s be FinSequence of D; :: thesis: ( 1 <= len s implies Op-Shift (s,1) = Op-LeftShift s )
assume AS: 1 <= len s ; :: thesis: Op-Shift (s,1) = Op-LeftShift s
R1: ( len (Op-Shift (s,1)) = len s & ( for i being Nat st i in Seg (len s) holds
(Op-Shift (s,1)) . i = s . ((((i - 1) + 1) mod (len s)) + 1) ) ) by defShift, AS;
R3: ( Op-LeftShift s is FinSequence of D & len (Op-LeftShift s) = len s ) by AS, LM003A;
R5: len <*(s . 1)*> = 1 by FINSEQ_1:40;
R6: len (s /^ 1) = (len s) - 1 by AS, RFINSEQ:def 1;

now :: thesis: for i being Nat st i in dom (Op-Shift (s,1)) holds
(Op-Shift (s,1)) . i = (Op-LeftShift s) . i

let i be Nat; :: thesis: ( i in dom (Op-Shift (s,1)) implies (Op-Shift (s,1)) . i = (Op-LeftShift s) . i )
assume i in dom (Op-Shift (s,1)) ; :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i
then P3: i in Seg (len s) by R1, FINSEQ_1:def 3;
then P31: ( 1 <= i & i <= len s ) by FINSEQ_1:1;

now :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i

per cases ( i = len s or i <> len s ) ;

suppose CS1: i = len s ; :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i

P35: (Op-Shift (s,1)) . i = s . ((((i - 1) + 1) mod (len s)) + 1) by P3, defShift, AS
.= s . (0 + 1) by AS, CS1, INT_1:62
.= s . 1 ;
Q39: i <= (len (s /^ 1)) + (len <*(s . 1)*>) by CS1, R6, R5;
Q40: i - (len (s /^ 1)) = (len s) - ((len s) - 1) by CS1, AS, RFINSEQ:def 1;
(Op-LeftShift s) . i = <*(s . 1)*> . 1 by Q39, R5, Q40, FINSEQ_1:23
.= s . 1 by FINSEQ_1:40 ;
hence (Op-Shift (s,1)) . i = (Op-LeftShift s) . i by P35; :: thesis: verum

end;

suppose i <> len s ; :: thesis: (Op-Shift (s,1)) . i = (Op-LeftShift s) . i

then ZZZ: ( 0 <= i & i < len s ) by P31, XXREAL_0:1;
i + 1 <= len s by ZZZ, NAT_1:13;
then Q38P: (i + 1) - 1 <= (len s) - 1 by XREAL_1:9;
then Q38: ( 1 <= i & i <= (len s) - 1 ) by P3, FINSEQ_1:1;
reconsider ls1 = (len s) - 1 as Element of NAT by Q38P, INT_1:3;
i in Seg ls1 by Q38, FINSEQ_1:1;
then Q39: i in dom (s /^ 1) by R6, FINSEQ_1:def 3;
Q37: (Op-Shift (s,1)) . i = s . ((((i - 1) + 1) mod (len s)) + 1) by P3, defShift, AS
.= s . (i + 1) by ZZZ, NAT_D:63 ;
(Op-LeftShift s) . i = (s /^ 1) . i by R6, Q38, FINSEQ_1:64
.= s . (i + 1) by Q39, AS, RFINSEQ:def 1 ;
hence (Op-Shift (s,1)) . i = (Op-LeftShift s) . i by Q37; :: thesis: verum

end;

end;

end;

hence (Op-Shift (s,1)) . i = (Op-LeftShift s) . i ; :: thesis: verum

end;

hence Op-Shift (s,1) = Op-LeftShift s by R1, R3, FINSEQ_2:9; :: thesis: verum