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 & 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:50;
then i - 1 < (len f) - (p .. f) by A3, XREAL_1:19;
then i -' 1 < (len f) - (p .. f) by A2, XREAL_1:233;
then (i -' 1) + (p .. f) < len f by XREAL_1:20;
then A6: ((i -' 1) + (p .. f)) + 1 <= len f by NAT_1:13;
(p .. f) - 1 >= 0 by A1, FINSEQ_4:21, XREAL_1:48;
then (len f) - ((p .. f) - 1) <= len f by XREAL_1:43;
then A7: i + 1 <= len f by A5, A4, XXREAL_0:2;
( i -' 1 >= 0 & 1 <= p .. f ) by A1, FINSEQ_4:21;
then A8: 0 + 1 <= (i -' 1) + (p .. f) by XREAL_1:7;
((i -' 1) + (p .. f)) + 1 = ((i -' 1) + 1) + (p .. f)
.= i + (p .. f) by A2, XREAL_1:235
.= ((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 3
.= LSeg (f,((i -' 1) + (p .. f))) by A8, A6, TOPREAL1:def 3 ;
:: thesis: verum