let p, q be FinSequence of D; :: thesis: ( len p = len s & ( for i being Nat st i in Seg (len s) holds
p . i = s . ((((i - 1) + n) mod (len s)) + 1) ) & len q = len s & ( for i being Nat st i in Seg (len s) holds
q . i = s . ((((i - 1) + n) mod (len s)) + 1) ) implies p = q )
assume A5: ( len p = len s & ( for i being Nat st i in Seg (len s) holds
p . i = s . ((((i - 1) + n) mod (len s)) + 1) ) ) ; :: thesis: ( not len q = len s or ex i being Nat st
( i in Seg (len s) & not q . i = s . ((((i - 1) + n) mod (len s)) + 1) ) or p = q )
assume A6: ( len q = len s & ( for i being Nat st i in Seg (len s) holds
q . i = s . ((((i - 1) + n) mod (len s)) + 1) ) ) ; :: thesis: p = q

now :: thesis: for j being Nat st j in dom p holds
p . j = q . j

let j be Nat; :: thesis: ( j in dom p implies p . j = q . j )
assume j in dom p ; :: thesis: p . j = q . j
then A7: j in Seg (len s) by A5, FINSEQ_1:def 3;
thus p . j = s . ((((j - 1) + n) mod (len s)) + 1) by A7, A5
.= q . j by A7, A6 ; :: thesis: verum

end;

hence p = q by A5, A6, FINSEQ_2:9; :: thesis: verum