let D be non empty set ; :: thesis:
let s be FinSequence of D; :: thesis:
let n, m be Integer; :: thesis:
assume A1: 1 <= len s ; :: thesis:
A2: ( len (Op-Shift (s,n)) = len s & ( for i being Nat st i in Seg (len s) holds
(Op-Shift (s,n)) . i = s . ((((i - 1) + n) mod (len s)) + 1) ) ) by Def3, A1;
A3: ( len (Op-Shift (s,(n + m))) = len s & ( for i being Nat st i in Seg (len s) holds
(Op-Shift (s,(n + m))) . i = s . ((((i - 1) + (n + m)) mod (len s)) + 1) ) ) by Def3, A1;
A4: len (Op-Shift ((Op-Shift (s,n)),m)) = len (Op-Shift (s,(n + m))) by A3, Def3, A1, A2;

now :: thesis:

let i be Nat; :: thesis:
assume A5: i in dom (Op-Shift ((Op-Shift (s,n)),m)) ; :: thesis:
then A6: i in Seg (len s) by A3, A4, FINSEQ_1:def 3;
A7: i in Seg (len (Op-Shift (s,n))) by A2, A3, A4, A5, FINSEQ_1:def 3;
reconsider i1 = ((i - 1) + m) mod (len s) as Element of NAT by INT_1:3, INT_1:57;
A8: 0 + 1 <= i1 + 1 by XREAL_1:6;
i1 + 1 <= len s by A1, INT_1:58, NAT_1:13;
then A9: i1 + 1 in Seg (len s) by A8;
A10: i1 mod (len s) = ((i - 1) + m) mod (len s) by NAT_D:65;
A11: (i1 + n) mod (len s) = ((((i - 1) + m) mod (len s)) + (n mod (len s))) mod (len s) by A10, NAT_D:66
.= (((i - 1) + m) + n) mod (len s) by NAT_D:66 ;
A12: (Op-Shift ((Op-Shift (s,n)),m)) . i = (Op-Shift (s,n)) . (i1 + 1) by A7, Def3, A1, A2
.= s . (((((i1 + 1) - 1) + n) mod (len s)) + 1) by A9, Def3, A1
.= s . (((((i - 1) + n) + m) mod (len s)) + 1) by A11 ;
(Op-Shift (s,(n + m))) . i = s . ((((i - 1) + (n + m)) mod (len s)) + 1) by A6, Def3, A1;
hence (Op-Shift ((Op-Shift (s,n)),m)) . i = (Op-Shift (s,(n + m))) . i by A12; :: thesis:

end;

hence Op-Shift ((Op-Shift (s,n)),m) = Op-Shift (s,(n + m)) by A4, FINSEQ_2:9; :: thesis: