let f be non constant standard special_circular_sequence; :: thesis: for q being Point of (TOP-REAL 2) st 1 < q .. f & q in rng f holds
(f /. 1) .. (Rotate f,q) = ((len f) + 1) - (q .. f)
let q be Point of (TOP-REAL 2); :: thesis: ( 1 < q .. f & q in rng f implies (f /. 1) .. (Rotate f,q) = ((len f) + 1) - (q .. f) )
assume that
A1: 1 < q .. f and
A2: q in rng f ; :: thesis: (f /. 1) .. (Rotate f,q) = ((len f) + 1) - (q .. f)
set i = (1 + (len f)) -' (q .. f);
A3: (q .. f) - 1 > 0 by A1, XREAL_1:52;
A4: q .. f <= len f by A2, FINSEQ_4:31;
then A5: q .. f <= (len f) + 1 by NAT_1:13;
then A6: (1 + (len f)) -' (q .. f) = (1 + (len f)) - (q .. f) by XREAL_1:235;
then ((1 + (len f)) -' (q .. f)) + ((q .. f) - 1) = len f ;
then (1 + (len f)) -' (q .. f) < len f by A3, XREAL_1:31;
then A7: (1 + (len f)) -' (q .. f) < len (Rotate f,q) by REVROT_1:14;

now

assume (q .. f) + 0 >= len f ; :: thesis: contradiction
then A8: q .. f = len f by A4, XXREAL_0:1;
q = f /. (q .. f) by A2, FINSEQ_5:41
.= f /. 1 by A8, FINSEQ_6:def 1 ;
hence contradiction by A1, FINSEQ_6:47; :: thesis: verum

end;

then A9: (len f) - (q .. f) > 0 by XREAL_1:22;
(1 + (len f)) -' (q .. f) = 1 + ((len f) - (q .. f)) by A6;
then A10: 1 + 0 < (1 + (len f)) -' (q .. f) by A9, XREAL_1:8;
then A11: (1 + (len f)) -' (q .. f) in dom (Rotate f,q) by A7, FINSEQ_3:27;
A12: f /. 1 = (Rotate f,q) /. ((1 + (len f)) -' (q .. f)) by A1, A2, REVROT_1:18;
then A13: f /. 1 = (Rotate f,q) . ((1 + (len f)) -' (q .. f)) by A11, PARTFUN1:def 8;
for j being set st j in dom (Rotate f,q) & j <> (1 + (len f)) -' (q .. f) holds
(Rotate f,q) . j <> f /. 1

proof

let z be set ; :: thesis: ( z in dom (Rotate f,q) & z <> (1 + (len f)) -' (q .. f) implies (Rotate f,q) . z <> f /. 1 )
assume that
A14: z in dom (Rotate f,q) and
A15: z <> (1 + (len f)) -' (q .. f) ; :: thesis: (Rotate f,q) . z <> f /. 1
reconsider j = z as Element of NAT by A14;

per cases ( j < (1 + (len f)) -' (q .. f) or (1 + (len f)) -' (q .. f) < j ) by A15, XXREAL_0:1;

suppose A16: j < (1 + (len f)) -' (q .. f) ; :: thesis: (Rotate f,q) . z <> f /. 1

1 <= j by A14, FINSEQ_3:27;
then (Rotate f,q) /. j <> f /. 1 by A12, A7, A16, GOBOARD7:38;
hence (Rotate f,q) . z <> f /. 1 by A14, PARTFUN1:def 8; :: thesis: verum

end;

suppose A17: (1 + (len f)) -' (q .. f) < j ; :: thesis: (Rotate f,q) . z <> f /. 1

j <= len (Rotate f,q) by A14, FINSEQ_3:27;
then (Rotate f,q) /. j <> f /. 1 by A12, A10, A17, GOBOARD7:39;
hence (Rotate f,q) . z <> f /. 1 by A14, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

then A18: Rotate f,q just_once_values f /. 1 by A11, A13, FINSEQ_4:9;
then (1 + (len f)) -' (q .. f) = (Rotate f,q) <- (f /. 1) by A11, A13, FINSEQ_4:def 3;
hence (f /. 1) .. (Rotate f,q) = (1 + (len f)) -' (q .. f) by A18, FINSEQ_4:35
.= ((len f) + 1) - (q .. f) by A5, XREAL_1:235 ;
:: thesis: verum