let D be non empty set ; :: thesis: for s being FinSequence of D
for n, m being Integer st 1 <= len s holds
Op-Shift ((Op-Shift (s,n)),m) = Op-Shift (s,(n + m))
let s be FinSequence of D; :: thesis: for n, m being Integer st 1 <= len s holds
Op-Shift ((Op-Shift (s,n)),m) = Op-Shift (s,(n + m))
let n, m be Integer; :: thesis: ( 1 <= len s implies Op-Shift ((Op-Shift (s,n)),m) = Op-Shift (s,(n + m)) )
assume AS: 1 <= len s ; :: thesis: Op-Shift ((Op-Shift (s,n)),m) = Op-Shift (s,(n + m))
P1: ( 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 defShift, AS;
P4: ( 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 defShift, AS;
P5: len (Op-Shift ((Op-Shift (s,n)),m)) = len (Op-Shift (s,(n + m))) by P4, defShift, AS, P1;

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

let i be Nat; :: thesis: ( i in dom (Op-Shift ((Op-Shift (s,n)),m)) implies (Op-Shift ((Op-Shift (s,n)),m)) . i = (Op-Shift (s,(n + m))) . i )
assume P9P: i in dom (Op-Shift ((Op-Shift (s,n)),m)) ; :: thesis: (Op-Shift ((Op-Shift (s,n)),m)) . i = (Op-Shift (s,(n + m))) . i
then P9: i in Seg (len s) by P4, P5, FINSEQ_1:def 3;
P10: i in Seg (len (Op-Shift (s,n))) by P1, P4, P5, P9P, FINSEQ_1:def 3;
reconsider i1 = ((i - 1) + m) mod (len s) as Element of NAT by INT_1:3, INT_1:57;
P21: 0 + 1 <= i1 + 1 by XREAL_1:6;
((i - 1) + m) mod (len s) < len s by AS, INT_1:58;
then i1 + 1 <= len s by NAT_1:13;
then P14: i1 + 1 in Seg (len s) by P21;
P17: i1 mod (len s) = ((i - 1) + m) mod (len s) by NAT_D:65;
P16: (i1 + n) mod (len s) = ((((i - 1) + m) mod (len s)) + (n mod (len s))) mod (len s) by P17, NAT_D:66
.= (((i - 1) + m) + n) mod (len s) by NAT_D:66 ;
P11: (Op-Shift ((Op-Shift (s,n)),m)) . i = (Op-Shift (s,n)) . (i1 + 1) by P10, defShift, AS, P1
.= s . (((((i1 + 1) - 1) + n) mod (len s)) + 1) by P14, defShift, AS
.= s . (((((i - 1) + n) + m) mod (len s)) + 1) by P16 ;
(Op-Shift (s,(n + m))) . i = s . ((((i - 1) + (n + m)) mod (len s)) + 1) by P9, defShift, AS;
hence (Op-Shift ((Op-Shift (s,n)),m)) . i = (Op-Shift (s,(n + m))) . i by P11; :: thesis: verum

end;

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