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 that
A1: p in rng f and
A2: q in rng f ; :: thesis: ( not p .. f < q .. f or p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f) )
assume A3: p .. f < q .. f ; :: thesis: p .. (Rotate f,q) = ((len f) + (p .. f)) - (q .. f)
then A4: p .. f = p .. (f -: q) by A1, A2, Th3;
A5: p in rng (f -: q) by A1, A2, A3, FINSEQ_5:49;
then A6: p .. (f -: q) >= 1 by FINSEQ_4:31;
A7: Rotate f,q = (f :- q) ^ ((f -: q) /^ 1) by A2, FINSEQ_6:def 2;

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

suppose A8: 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 A2, A3, A8, Th9; :: thesis: verum

end;

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

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

end;

end;