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;

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 A3: i in Seg (len s) by A2, FINSEQ_1:def 3;
then A4: ( 1 <= i & i <= len s ) by FINSEQ_1:1;
then A5: 1 - 1 <= i - 1 by XREAL_1:9;
i < (len s) + 1 by A4, NAT_1:13;
then A6: 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 A1, INT_1:62
.= ((i - 1) mod (len s)) + 1 by NAT_D:65
.= (i - 1) + 1 by A6, A5, NAT_D:63
.= i ;
hence (Op-Shift (s,(len s))) . i = s . i by A3, Def3, A1; :: thesis: verum

end;

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