let i be Element of NAT ; for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds
LSeg (Rotate f,p),i = LSeg f,((i + (p .. f)) -' (len f))
let p be Point of (TOP-REAL 2); for f being circular FinSequence of (TOP-REAL 2) st p in rng f & len (f :- p) <= i & i < len f holds
LSeg (Rotate f,p),i = LSeg f,((i + (p .. f)) -' (len f))
let f be circular FinSequence of (TOP-REAL 2); ( p in rng f & len (f :- p) <= i & i < len f implies LSeg (Rotate f,p),i = LSeg f,((i + (p .. f)) -' (len f)) )
assume that
A1:
p in rng f
and
A2:
len (f :- p) <= i
and
A3:
i < len f
; LSeg (Rotate f,p),i = LSeg f,((i + (p .. f)) -' (len f))
A4:
p .. f <= len f
by A1, FINSEQ_4:31;
A5:
len (f :- p) = ((len f) - (p .. f)) + 1
by A1, FINSEQ_5:53;
then
((len f) -' (p .. f)) + 1 <= i
by A2, A4, XREAL_1:235;
then
((len f) + 1) -' (p .. f) <= i
by A4, NAT_D:38;
then A6:
(len f) + 1 <= i + (p .. f)
by NAT_D:52;
then A7:
1 <= (i + (p .. f)) -' (len f)
by NAT_D:55;
(len f) - (p .. f) >= 0
by A4, XREAL_1:50;
then
((len f) - (p .. f)) + 1 >= 0 + 1
by XREAL_1:8;
then A8:
0 + 1 <= 0 + i
by A2, A5, XXREAL_0:2;
A9:
len (Rotate f,p) = len f
by Th14;
A10:
len f <= (len f) + 1
by NAT_1:11;
A11:
i + 1 <= len f
by A3, NAT_1:13;
then
(i + 1) + (p .. f) <= (len f) + (len f)
by A4, XREAL_1:9;
then
((i + (p .. f)) + 1) -' (len f) <= len f
by NAT_D:53;
then A12:
((i + (p .. f)) -' (len f)) + 1 <= len f
by A6, A10, NAT_D:38, XXREAL_0:2;
((i + 1) + (p .. f)) -' (len f) =
((i + (p .. f)) + 1) -' (len f)
.=
((i + (p .. f)) -' (len f)) + 1
by A6, A10, NAT_D:38, XXREAL_0:2
;
then A13:
(Rotate f,p) /. (i + 1) = f /. (((i + (p .. f)) -' (len f)) + 1)
by A1, A2, A11, Th17, NAT_1:12;
( i + 1 <= len f & (Rotate f,p) /. i = f /. ((i + (p .. f)) -' (len f)) )
by A1, A2, A3, Th17, NAT_1:13;
hence LSeg (Rotate f,p),i =
LSeg (f /. ((i + (p .. f)) -' (len f))),(f /. (((i + (p .. f)) -' (len f)) + 1))
by A9, A13, A8, TOPREAL1:def 5
.=
LSeg f,((i + (p .. f)) -' (len f))
by A7, A12, TOPREAL1:def 5
;
verum