let D be non empty set ; :: thesis:
let p2, p1 be Element of D; :: thesis:
let f be FinSequence of D; :: thesis:

per cases ;

suppose A1: p1 in rng f ; :: thesis:

assume that
A2: f is circular and
A3: f just_once_values p2 ; :: thesis:
A4: p2 in rng f by A3, FINSEQ_4:60;

now

per cases ;

suppose rng f is trivial ; :: thesis:

then p1 = p2 by A1, A4, REALSET1:14;
hence Rotate (Rotate f,p1),p2 = Rotate f,p2 by Th99; :: thesis:

end;

suppose A5: not rng f is trivial ; :: thesis:

then f = <*(f /. 1)*> ^ (f /^ 1) by FINSEQ_5:32, RELAT_1:60;
then A6: rng f = (rng <*(f /. 1)*>) \/ (rng (f /^ 1)) by FINSEQ_1:44;

now

assume A7: not p2 in rng (f /^ 1) ; :: thesis:
then p2 in rng <*(f /. 1)*> by A4, A6, XBOOLE_0:def 3;
then p2 in {(f /. 1)} by FINSEQ_1:56;
then p2 = f /. 1 by TARSKI:def 1;
then A8: p2 = f /. (len f) by A2, Def1;
not f is trivial by A5;
then len f >= 1 + 1 by REALSET1:13;
then A9: 1 < len f by NAT_1:13;
len f in dom f by A5, FINSEQ_5:6, RELAT_1:60;
hence contradiction by A7, A8, A9, Th63; :: thesis:

end;

hence Rotate (Rotate f,p1),p2 = Rotate f,p2 by A3, Th110; :: thesis:

end;

end;

end;

hence Rotate (Rotate f,p1),p2 = Rotate f,p2 ; :: thesis:

end;

suppose not p1 in rng f ; :: thesis:

hence ( f is circular & f just_once_values p2 implies Rotate (Rotate f,p1),p2 = Rotate f,p2 ) by Def2; :: thesis:

end;

end;