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 AS: 1 <= len s ; :: thesis: Op-Shift (s,(- (len s))) = s
set m = len s;
P1: ( 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 defShift, AS;
- (len s) = (len s) * (- 1) ;
then P11P: ( 0 < len s & len s divides - (len s) ) by AS, 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 P3: i in Seg (len s) by P1, FINSEQ_1:def 3;
then P31: ( 1 <= i & i <= len s ) by FINSEQ_1:1;
then P32: 1 - 1 <= i - 1 by XREAL_1:9;
i < (len s) + 1 by P31, NAT_1:13;
then P33: 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 P11P, INT_1:62
.= ((i - 1) mod (len s)) + 1 by NAT_D:65
.= (i - 1) + 1 by P33, P32, NAT_D:63
.= i ;
hence (Op-Shift (s,(- (len s)))) . i = s . i by defShift, AS, P3; :: thesis: verum

end;

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