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 & 1 <= i & i < len (f :- p) holds
LSeg (Rotate f,p),i = LSeg f,((i -' 1) + (p .. f))
let p be Point of (TOP-REAL 2); :: thesis: for f being FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < len (f :- p) holds
LSeg (Rotate f,p),i = LSeg f,((i -' 1) + (p .. f))
let f be FinSequence of (TOP-REAL 2); :: thesis: ( p in rng f & 1 <= i & i < len (f :- p) implies LSeg (Rotate f,p),i = LSeg f,((i -' 1) + (p .. f)) )
assume that
A1: p in rng f and
A2: 1 <= i and
A3: i < len (f :- p) ; :: thesis: LSeg (Rotate f,p),i = LSeg f,((i -' 1) + (p .. f))
A4: i + 1 <= len (f :- p) by A3, NAT_1:13;
A5: len (f :- p) = ((len f) - (p .. f)) + 1 by A1, FINSEQ_5:53;
then i - 1 < (len f) - (p .. f) by A3, XREAL_1:21;
then i -' 1 < (len f) - (p .. f) by A2, XREAL_1:235;
then (i -' 1) + (p .. f) < len f by XREAL_1:22;
then A6: ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13;
(p .. f) - 1 >= 0 by A1, FINSEQ_4:31, XREAL_1:50;
then (len f) - ((p .. f) - 1) <= len f by XREAL_1:45;
then A7: i + 1 <= len f by A5, A4, XXREAL_0:2;
( i -' 1 >= 0 & 1 <= p .. f ) by A1, FINSEQ_4:31, NAT_1:2;
then A8: 0 + 1 <= (i -' 1) + (p .. f) by XREAL_1:9;
((i -' 1) + (p .. f)) + 1 = ((i -' 1) + 1) + (p .. f)
.= i + (p .. f) by A2, XREAL_1:237
.= ((i + 1) -' 1) + (p .. f) by NAT_D:34 ;
then A9: (Rotate f,p) /. (i + 1) = f /. (((i -' 1) + (p .. f)) + 1) by A1, A4, Th9, NAT_1:11;
A10: len (Rotate f,p) = len f by Th14;
(Rotate f,p) /. i = f /. ((i -' 1) + (p .. f)) by A1, A2, A3, Th9;
hence LSeg (Rotate f,p),i = LSeg (f /. ((i -' 1) + (p .. f))),(f /. (((i -' 1) + (p .. f)) + 1)) by A2, A10, A9, A7, TOPREAL1:def 5
.= LSeg f,((i -' 1) + (p .. f)) by A8, A6, TOPREAL1:def 5 ;
:: thesis: verum