let D be non empty set ; :: thesis: for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,(- 1)) = Op-RightShift s
let s be FinSequence of D; :: thesis: ( 1 <= len s implies Op-Shift (s,(- 1)) = Op-RightShift s )
assume AS: 1 <= len s ; :: thesis: Op-Shift (s,(- 1)) = Op-RightShift 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-RightShift s is FinSequence of D & len (Op-RightShift s) = len s ) by AS, LM004A;
R5: len <*(s . (len s))*> = 1 by FINSEQ_1:40;

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

let i be Nat; :: thesis: ( i in dom (Op-Shift (s,(- 1))) implies (Op-Shift (s,(- 1))) . i = (Op-RightShift s) . i )
assume i in dom (Op-Shift (s,(- 1))) ; :: thesis: (Op-Shift (s,(- 1))) . i = (Op-RightShift 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;
i < (len s) + 1 by P31, NAT_1:13;
then DD1: i - 1 < ((len s) + 1) - 1 by XREAL_1:14;

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

per cases ( i = 1 or i <> 1 ) ;

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

P34P: - 1 >= - (len s) by AS, XREAL_1:24;
P35: (Op-Shift (s,(- 1))) . i = s . ((((i - 1) - 1) mod (len s)) + 1) by P3, defShift, AS
.= s . (((len s) + (- 1)) + 1) by P34P, CS1, NAT_D:63
.= s . (len s) ;
(Op-RightShift s) . i = (<*(s . (len s))*> ^ s) . i by P3, FUNCT_1:49
.= <*(s . (len s))*> . i by CS1, R5, FINSEQ_1:64
.= s . (len s) by CS1, FINSEQ_1:40 ;
hence (Op-Shift (s,(- 1))) . i = (Op-RightShift s) . i by P35; :: thesis: verum

end;

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

then Q35P: 1 < i by P31, XXREAL_0:1;
then Q35: 1 + 1 <= i by NAT_1:13;
(i - 1) - 1 <= i - 1 by XREAL_1:43;
then Q36P: ( 0 <= i - 2 & i - 2 < len s ) by Q35, DD1, XREAL_1:48, XXREAL_0:2;
Q37: (Op-Shift (s,(- 1))) . i = s . ((((i - 1) - 1) mod (len s)) + 1) by P3, defShift, AS
.= s . ((i - 2) + 1) by Q36P, NAT_D:63
.= s . (i - 1) ;
Q38: (len <*(s . (len s))*>) + 1 <= i by Q35P, R5, NAT_1:13;
Q39: i <= (len <*(s . (len s))*>) + (len s) by P31, R5, NAT_1:13;
(Op-RightShift s) . i = (<*(s . (len s))*> ^ s) . i by P3, FUNCT_1:49
.= s . (i - 1) by Q38, Q39, R5, FINSEQ_1:23 ;
hence (Op-Shift (s,(- 1))) . i = (Op-RightShift s) . i by Q37; :: thesis: verum

end;

end;

end;

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

end;

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