let f be V19() standard special_circular_sequence; 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); ( 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
; ( not p .. f < q .. f or p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f) )
assume A3:
p .. f < q .. f
; 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:46;
then A6:
p .. (f -: q) >= 1
by FINSEQ_4:21;
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 A9:
p .. f > 1
;
p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f)then A10:
p .. f = 1
+ (p .. ((f -: q) /^ 1))
by A5, A4, FINSEQ_6:56;
not
p in {q}
by A3, TARSKI:def 1;
then A11:
not
p in rng <*q*>
by FINSEQ_1:38;
A12:
q in rng (f /^ 1)
by A2, A3, A9, FINSEQ_6:78;
then ((f /^ 1) -| q) ^ <*q*> =
(f /^ 1) | (q .. (f /^ 1))
by FINSEQ_5:24
.=
(f /^ 1) -: q
by FINSEQ_5:def 1
;
then A13:
rng ((f /^ 1) -: q) = (rng ((f /^ 1) -| q)) \/ (rng <*q*>)
by FINSEQ_1:31;
A14:
rng ((f /^ 1) -| q) misses rng ((f /^ 1) |-- q)
by A12, FINSEQ_4:57;
(f /^ 1) :- q = <*q*> ^ ((f /^ 1) |-- q)
by A12, FINSEQ_6:41;
then A15:
rng ((f /^ 1) :- q) = (rng <*q*>) \/ (rng ((f /^ 1) |-- q))
by FINSEQ_1:31;
p .. (f -: q) > 1
by A1, A2, A3, A9, Th3;
then A16:
p in rng ((f -: q) /^ 1)
by A5, FINSEQ_6:57;
then
p in rng ((f /^ 1) -: q)
by A2, A3, A9, FINSEQ_6:60;
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:83;
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:7
.=
(((len f) - (q .. f)) + 1) + ((p .. f) - 1)
by A2, A10, FINSEQ_5:50
.=
((len f) + (p .. f)) - (q .. f)
;
verum end;