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 A1: ( 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 A2: ( 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 A32: j in Seg (len s) by A1, FINSEQ_1:def 3;
thus p . j = s . ((((j - 1) + n) mod (len s)) + 1) by A32, A1
.= q . j by A32, A2 ; :: thesis: verum

end;

hence p = q by A1, A2, FINSEQ_2:9; :: thesis: verum