let i be Nat; :: thesis: for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds
LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f)))
let p be Point of (TOP-REAL 2); :: thesis: for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds
LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f)))
let f be circular FinSequence of (TOP-REAL 2); :: thesis: ( p in rng f & len (f :- p) <= i & i < len f implies LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f))) )
assume that
A1: p in rng f and
A2: len (f :- p) <= i and
A3: i < len f ; :: thesis: LSeg ((Rotate (f,p)),i) = LSeg (f,((i + (p .. f)) -' (len f)))
A4: p .. f <= len f by A1, FINSEQ_4:21;
A5: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:50;
then ((len f) -' (p .. f)) + 1 <= i by A2, A4, XREAL_1:233;
then ((len f) + 1) -' (p .. f) <= i by A4, NAT_D:38;
then A6: (len f) + 1 <= i + (p .. f) by NAT_D:52;
then A7: 1 <= (i + (p .. f)) -' (len f) by NAT_D:55;
(len f) - (p .. f) >= 0 by A4, XREAL_1:48;
then ((len f) - (p .. f)) + 1 >= 0 + 1 by XREAL_1:6;
then A8: 0 + 1 <= 0 + i by A2, A5, XXREAL_0:2;
A9: len (Rotate (f,p)) = len f by Th14;
A10: len f <= (len f) + 1 by NAT_1:11;
A11: i + 1 <= len f by A3, NAT_1:13;
then (i + 1) + (p .. f) <= (len f) + (len f) by A4, XREAL_1:7;
then ((i + (p .. f)) + 1) -' (len f) <= len f by NAT_D:53;
then A12: ((i + (p .. f)) -' (len f)) + 1 <= len f by A6, A10, NAT_D:38, XXREAL_0:2;
((i + 1) + (p .. f)) -' (len f) = ((i + (p .. f)) + 1) -' (len f)
.= ((i + (p .. f)) -' (len f)) + 1 by A6, A10, NAT_D:38, XXREAL_0:2 ;
then A13: (Rotate (f,p)) /. (i + 1) = f /. (((i + (p .. f)) -' (len f)) + 1) by A1, A2, A11, Th17, NAT_1:12;
( i + 1 <= len f & (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) ) by A1, A2, A3, Th17, NAT_1:13;
hence LSeg ((Rotate (f,p)),i) = LSeg ((f /. ((i + (p .. f)) -' (len f))),(f /. (((i + (p .. f)) -' (len f)) + 1))) by A9, A13, A8, TOPREAL1:def 3
.= LSeg (f,((i + (p .. f)) -' (len f))) by A7, A12, TOPREAL1:def 3 ;
:: thesis: verum