let f be non constant standard special_circular_sequence; :: thesis: for p, q being Point of (TOP-REAL 2) st p in rng f & q in rng f & p .. f < q .. f holds
p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f)
let p, q be Point of (TOP-REAL 2); :: thesis: ( p in rng f & q in rng f & p .. f < q .. f implies p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f) )
assume A1: ( p in rng f & q in rng f ) ; :: thesis: ( not p .. f < q .. f or p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f) )
then A2: Rotate f,q = (f :- q) ^ ((f -: q) /^ 1) by FINSEQ_6:def 2;
assume A3: p .. f < q .. f ; :: thesis: p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f)
then A4: p in rng (f -: q) by A1, FINSEQ_5:49;
then A5: p .. (f -: q) >= 1 by FINSEQ_4:31;
A6: p .. f = p .. (f -: q) by A1, A3, Th3;

per cases ( p .. f = 1 or p .. f > 1 ) by A5, A6, XXREAL_0:1;

suppose A7: p .. f = 1 ; :: thesis: p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f)

then p = f /. 1 by A1, FINSEQ_5:41;
hence p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f) by A1, A3, A7, Th9; :: thesis: verum

end;

suppose A8: p .. f > 1 ; :: thesis: p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f)

then A9: p .. (f -: q) > 1 by A1, A3, Th3;
A10: p .. f = 1 + (p .. ((f -: q) /^ 1)) by A4, A6, A8, FINSEQ_6:61;
A11: f /^ 1 is one-to-one by Th8;
A12: p in rng ((f -: q) /^ 1) by A4, A9, FINSEQ_6:62;
then A13: p in rng ((f /^ 1) -: q) by A1, A3, A8, FINSEQ_6:65;
A14: q in rng (f /^ 1) by A1, A3, A8, FINSEQ_6:83;
then A15: rng ((f /^ 1) -| q) misses rng ((f /^ 1) |-- q) by A11, FINSEQ_4:72;
((f /^ 1) -| q) ^ <*q*> = (f /^ 1) | (q .. (f /^ 1)) by A14, FINSEQ_5:27
.= (f /^ 1) -: q by FINSEQ_5:def 1 ;
then A16: rng ((f /^ 1) -: q) = (rng ((f /^ 1) -| q)) \/ (rng <*q*>) by FINSEQ_1:44;
not p in {q} by A3, TARSKI:def 1;
then A17: not p in rng <*q*> by FINSEQ_1:55;
then p in rng ((f /^ 1) -| q) by A13, A16, XBOOLE_0:def 3;
then A18: not p in rng ((f /^ 1) |-- q) by A15, XBOOLE_0:3;
(f /^ 1) :- q = <*q*> ^ ((f /^ 1) |-- q) by A14, FINSEQ_6:45;
then rng ((f /^ 1) :- q) = (rng <*q*>) \/ (rng ((f /^ 1) |-- q)) by FINSEQ_1:44;
then not p in rng ((f /^ 1) :- q) by A17, A18, XBOOLE_0:def 3;
then not p in rng (f :- q) by A1, A3, A8, FINSEQ_6:89;
then p in (rng ((f -: q) /^ 1)) \ (rng (f :- q)) by A12, XBOOLE_0:def 5;
hence p .. (Rotate f,q) = (len (f :- q)) + (p .. ((f -: q) /^ 1)) by A2, FINSEQ_6:9
.= (((len f) - (q .. f)) + 1) + ((p .. f) - 1) by A1, A10, FINSEQ_5:53
.= ((len f) + (p .. f)) - (q .. f) ;
:: thesis: verum

end;

end;