let i be Element of 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:11;
then i -' (p .. f) < (len f) - (p .. f) by A2, XREAL_1:235;
then (i -' (p .. f)) + 1 < ((len f) - (p .. f)) + 1 by XREAL_1:8;
then A4: (i -' (p .. f)) + 1 < len (f :- p) by A1, FINSEQ_5:53;
1 + (p .. f) <= i + 1 by A2, XREAL_1:8;
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:237 ;
hence LSeg f,i = LSeg (Rotate f,p),((i -' (p .. f)) + 1) by A1, A5, A4, Th24; :: thesis: verum