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 & 1 <= i & i < p .. f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
let p be Point of (TOP-REAL 2); :: thesis: for f being circular FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < p .. f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
let f be circular FinSequence of (TOP-REAL 2); :: thesis: ( p in rng f & 1 <= i & i < p .. f implies LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) )
assume that
A1: p in rng f and
A2: 1 <= i and
A3: i < p .. f ; :: thesis: LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
A4: p .. f <= len f by A1, FINSEQ_4:21;
A5: i + (len f) < (len f) + (p .. f) by A3, XREAL_1:6;
A6: len f <= i + (len f) by NAT_1:11;
then p .. f <= i + (len f) by A4, XXREAL_0:2;
then A7: (i + (len f)) -' (p .. f) < len f by A5, NAT_D:54;
(len f) + 1 <= i + (len f) by A2, XREAL_1:6;
then ((len f) + 1) -' (p .. f) <= (i + (len f)) -' (p .. f) by NAT_D:42;
then ((len f) -' (p .. f)) + 1 <= (i + (len f)) -' (p .. f) by A4, NAT_D:38;
then ((len f) - (p .. f)) + 1 <= (i + (len f)) -' (p .. f) by A4, XREAL_1:233;
then A8: len (f :- p) <= (i + (len f)) -' (p .. f) by A1, FINSEQ_5:50;
(((i + (len f)) -' (p .. f)) + (p .. f)) -' (len f) = (i + (len f)) -' (len f) by A4, A6, XREAL_1:235, XXREAL_0:2
.= i by NAT_D:34 ;
hence LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) by A1, A8, A7, Th31; :: thesis: verum