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 A1: 1 <= len s ; :: thesis: Op-Shift (s,(- 1)) = Op-RightShift s
A2: ( 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 Def3, A1;
A3: ( Op-RightShift s is FinSequence of D & len (Op-RightShift s) = len s ) by A1, Th8, Th7;
A4: 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 A5: i in Seg (len s) by A2, FINSEQ_1:def 3;
then A6: ( 1 <= i & i <= len s ) by FINSEQ_1:1;
i < (len s) + 1 by A6, NAT_1:13;
then A7: 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 A8: i = 1 ; :: thesis: (Op-Shift (s,(- 1))) . i = (Op-RightShift s) . i

A9: - 1 >= - (len s) by A1, XREAL_1:24;
A10: (Op-Shift (s,(- 1))) . i = s . ((((i - 1) - 1) mod (len s)) + 1) by A5, Def3, A1
.= s . (((len s) + (- 1)) + 1) by A9, A8, NAT_D:63
.= s . (len s) ;
(Op-RightShift s) . i = (<*(s . (len s))*> ^ s) . i by A5, FUNCT_1:49
.= <*(s . (len s))*> . i by A8, A4, FINSEQ_1:64
.= s . (len s) by A8 ;
hence (Op-Shift (s,(- 1))) . i = (Op-RightShift s) . i by A10; :: thesis: verum

end;

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

then A11: 1 < i by A6, XXREAL_0:1;
then A12: 1 + 1 <= i by NAT_1:13;
(i - 1) - 1 <= i - 1 by XREAL_1:43;
then A13: ( 0 <= i - 2 & i - 2 < len s ) by A12, A7, XREAL_1:48, XXREAL_0:2;
A14: (Op-Shift (s,(- 1))) . i = s . ((((i - 1) - 1) mod (len s)) + 1) by A5, Def3, A1
.= s . ((i - 2) + 1) by A13, NAT_D:63
.= s . (i - 1) ;
A15: (len <*(s . (len s))*>) + 1 <= i by A11, A4, NAT_1:13;
A16: i <= (len <*(s . (len s))*>) + (len s) by A6, A4, NAT_1:13;
(Op-RightShift s) . i = (<*(s . (len s))*> ^ s) . i by A5, FUNCT_1:49
.= s . (i - 1) by A15, A16, A4, FINSEQ_1:23 ;
hence (Op-Shift (s,(- 1))) . i = (Op-RightShift s) . i by A14; :: 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 A2, A3, FINSEQ_2:9; :: thesis: verum