let i be Nat; :: thesis: for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st p in rng f & p .. f <= i & i < len f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1))
let p be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2) st p in rng f & p .. f <= i & i < len f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1))
let f be FinSequence of (TOP-REAL 2); :: thesis: ( p in rng f & p .. f <= i & i < len f implies LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) )
assume that
A1: p in rng f and
A2: p .. f <= i and
A3: i < len f ; :: thesis: LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1))
i - (p .. f) < (len f) - (p .. f) by A3, XREAL_1:9;
then i -' (p .. f) < (len f) - (p .. f) by A2, XREAL_1:233;
then (i -' (p .. f)) + 1 < ((len f) - (p .. f)) + 1 by XREAL_1:6;
then A4: (i -' (p .. f)) + 1 < len (f :- p) by A1, FINSEQ_5:50;
1 + (p .. f) <= i + 1 by A2, XREAL_1:6;
then 1 <= (i + 1) -' (p .. f) by NAT_D:55;
then A5: 1 <= (i -' (p .. f)) + 1 by A2, NAT_D:38;
(((i -' (p .. f)) + 1) -' 1) + (p .. f) = (i -' (p .. f)) + (p .. f) by NAT_D:34
.= i by A2, XREAL_1:235 ;
hence LSeg (f,i) = LSeg ((Rotate (f,p)),((i -' (p .. f)) + 1)) by A1, A5, A4, Th24; :: thesis: verum