let f be V19() 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:50;
A4: q .. f <= len f by A2, FINSEQ_4:21;
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:233;
then ((1 + (len f)) -' (q .. f)) + ((q .. f) - 1) = len f ;
then (1 + (len f)) -' (q .. f) < len f by A3, XREAL_1:29;
then A7: (1 + (len f)) -' (q .. f) < len (Rotate (f,q)) by FINSEQ_6:179;
now :: thesis: not (q .. f) + 0 >= len f
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:38
.= f /. 1 by A8, FINSEQ_6:def 1 ;
hence contradiction by A1, FINSEQ_6:43; :: thesis: verum
end;
then A9: (len f) - (q .. f) > 0 by XREAL_1:20;
(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:6;
then A11: (1 + (len f)) -' (q .. f) in dom (Rotate (f,q)) by A7, FINSEQ_3:25;
A12: f /. 1 = (Rotate (f,q)) /. ((1 + (len f)) -' (q .. f)) by A1, A2, FINSEQ_6:183;
then A13: f /. 1 = (Rotate (f,q)) . ((1 + (len f)) -' (q .. f)) by A11, PARTFUN1:def 6;
for j being object st j in dom (Rotate (f,q)) & j <> (1 + (len f)) -' (q .. f) holds
(Rotate (f,q)) . j <> f /. 1
proof
let z be object ; :: 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 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:25;
then (Rotate (f,q)) /. j <> f /. 1 by A12, A7, A16, GOBOARD7:36;
hence (Rotate (f,q)) . z <> f /. 1 by A14, PARTFUN1:def 6; :: 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:25;
then (Rotate (f,q)) /. j <> f /. 1 by A12, A10, A17, GOBOARD7:37;
hence (Rotate (f,q)) . z <> f /. 1 by A14, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
then A18: Rotate (f,q) just_once_values f /. 1 by A11, A13, FINSEQ_4:7;
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:25
.= ((len f) + 1) - (q .. f) by A5, XREAL_1:233 ;
:: thesis: verum