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: p2 in rng (f /^ 1) and
A3: f just_once_values p2 ; :: thesis:
A4: p2 in rng f by A3, FINSEQ_4:7;
f = ((f -| p1) ^ <*p1*>) ^ (f |-- p1) by A1, FINSEQ_4:66;
then A5: p2 in (rng ((f -| p1) ^ <*p1*>)) \+\ (rng (f |-- p1)) by A3, Th19;

A6: now

per cases by A5, XBOOLE_0:1;

case that p2 in rng ((f -| p1) ^ <*p1*>) and
A7: not p2 in rng (f |-- p1) ; :: thesis:

now

per cases ;

case not p2 in rng <*p1*> ; :: thesis:

then not p2 in (rng (f |-- p1)) \/ (rng <*p1*>) by A7, XBOOLE_0:def 3;
then not p2 in rng (<*p1*> ^ (f |-- p1)) by FINSEQ_1:44;
hence not p2 in rng (f :- p1) by A1, Th45; :: thesis:

end;

case p2 in rng <*p1*> ; :: thesis:

then p2 in {p1} by FINSEQ_1:56;
hence p2 = p1 by TARSKI:def 1; :: thesis:

end;

end;

end;

hence ( p2 in rng (f :- p1) implies p1 = p2 ) ; :: thesis:

end;

case not p2 in rng ((f -| p1) ^ <*p1*>) ; :: thesis:

hence not p2 in rng (f -: p1) by A1, Th44; :: thesis:

end;

end;

end;

f = <*(f /. 1)*> ^ (f /^ 1) by A4, FINSEQ_5:32, RELAT_1:60;
then p2 in (rng <*(f /. 1)*>) \+\ (rng (f /^ 1)) by A3, Th19;
then not p2 in rng <*(f /. 1)*> by A2, XBOOLE_0:1;
then not p2 in {(f /. 1)} by FINSEQ_1:56;
then p2 <> f /. 1 by TARSKI:def 1;
then A8: p2 .. f <> 1 by A4, FINSEQ_5:41;

now

per cases by A4, A6, XBOOLE_0:def 5;

suppose p1 = p2 ; :: thesis:

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

end;

suppose p2 in (rng f) \ (rng (f -: p1)) ; :: thesis:

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

end;

suppose p2 in (rng f) \ (rng (f :- p1)) ; :: thesis:

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

end;

end;

end;

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

end;

suppose not p1 in rng f ; :: thesis:

hence ( p2 in rng (f /^ 1) & f just_once_values p2 implies Rotate (Rotate f,p1),p2 = Rotate f,p2 ) by Def2; :: thesis:

end;

end;