let D be non empty set ; :: thesis: for s being FinSequence of D st 1 <= len s holds
Op-Shift (s,(- (len s))) = s
let s be FinSequence of D; :: thesis: ( 1 <= len s implies Op-Shift (s,(- (len s))) = s )
assume A1: 1 <= len s ; :: thesis: Op-Shift (s,(- (len s))) = s
set m = len s;
A2: ( len (Op-Shift (s,(- (len s)))) = len s & ( for i being Nat st i in Seg (len s) holds
(Op-Shift (s,(- (len s)))) . i = s . ((((i - 1) + (- (len s))) mod (len s)) + 1) ) ) by Def3, A1;
- (len s) = (len s) * (- 1) ;
then A3: ( 0 < len s & len s divides - (len s) ) by A1, INT_1:def 3;

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

let i be Nat; :: thesis: ( i in dom (Op-Shift (s,(- (len s)))) implies (Op-Shift (s,(- (len s)))) . i = s . i )
assume i in dom (Op-Shift (s,(- (len s)))) ; :: thesis: (Op-Shift (s,(- (len s)))) . i = s . i
then A4: i in Seg (len s) by A2, FINSEQ_1:def 3;
then A5: ( 1 <= i & i <= len s ) by FINSEQ_1:1;
then A6: 1 - 1 <= i - 1 by XREAL_1:9;
i < (len s) + 1 by A5, NAT_1:13;
then A7: i - 1 < ((len s) + 1) - 1 by XREAL_1:14;
(((i - 1) + (- (len s))) mod (len s)) + 1 = ((((i - 1) mod (len s)) + ((- (len s)) mod (len s))) mod (len s)) + 1 by NAT_D:66
.= ((((i - 1) mod (len s)) + 0) mod (len s)) + 1 by A3, INT_1:62
.= ((i - 1) mod (len s)) + 1 by NAT_D:65
.= (i - 1) + 1 by A7, A6, NAT_D:63
.= i ;
hence (Op-Shift (s,(- (len s)))) . i = s . i by Def3, A1, A4; :: thesis: verum

end;

hence Op-Shift (s,(- (len s))) = s by A2, FINSEQ_2:9; :: thesis: verum