let p be Point of (TOP-REAL 2); :: thesis:
let f be V8() standard special_circular_sequence; :: thesis:

per cases ;

suppose not p in rng f ; :: thesis:

then ( Rotate f,p = f & not p in rng (Rev f) ) by FINSEQ_5:60, FINSEQ_6:def 2;
hence Rev (Rotate f,p) = Rotate (Rev f),p by FINSEQ_6:def 2; :: thesis:

end;

suppose A1: p = f /. 1 ; :: thesis:

then A2: p = (Rev f) /. (len f) by FINSEQ_5:68
.= (Rev f) /. (len (Rev f)) by FINSEQ_5:def 3
.= (Rev f) /. 1 by FINSEQ_6:def 1 ;
Rotate f,p = f by A1, FINSEQ_6:95;
hence Rev (Rotate f,p) = Rotate (Rev f),p by A2, FINSEQ_6:95; :: thesis:

end;

suppose that A3: p in rng f and
A4: p <> f /. 1 ; :: thesis:

f just_once_values p

proof

take p .. f ; :: according to REVROT_1:def 2 :: thesis:
thus A5: p .. f in dom f by A3, FINSEQ_4:30; :: thesis:
thus A6: p = f . (p .. f) by A3, FINSEQ_4:29
.= f /. (p .. f) by A5, PARTFUN1:def 8 ; :: thesis:
let z be set ; :: thesis:
assume that
A7: z in dom f and
A8: z <> p .. f ; :: thesis:
reconsider k = z as Element of NAT by A7;

per cases by A8, XXREAL_0:1;

suppose A9: k < p .. f ; :: thesis:

( p .. f <= len f & p .. f <> len f ) by A3, A4, A6, FINSEQ_4:31, FINSEQ_6:def 1;
then A10: p .. f < len f by XXREAL_0:1;
1 <= k by A7, FINSEQ_3:27;
hence f /. z <> p by A6, A9, A10, GOBOARD7:38; :: thesis:

end;

suppose A11: k > p .. f ; :: thesis:

p .. f >= 1 by A3, FINSEQ_4:31;
then A12: p .. f > 1 by A4, A6, XXREAL_0:1;
k <= len f by A7, FINSEQ_3:27;
hence f /. z <> p by A6, A11, A12, GOBOARD7:39; :: thesis:

end;

end;

end;

hence Rev (Rotate f,p) = Rotate (Rev f),p by FINSEQ_6:112; :: thesis:

end;

end;