let i be Nat; for p being Point of (TOP-REAL 2)
for f being circular FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < p .. f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
let p be Point of (TOP-REAL 2); for f being circular FinSequence of (TOP-REAL 2) st p in rng f & 1 <= i & i < p .. f holds
LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
let f be circular FinSequence of (TOP-REAL 2); ( p in rng f & 1 <= i & i < p .. f implies LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f))) )
assume that
A1:
p in rng f
and
A2:
1 <= i
and
A3:
i < p .. f
; LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
A4:
p .. f <= len f
by A1, FINSEQ_4:21;
A5:
i + (len f) < (len f) + (p .. f)
by A3, XREAL_1:6;
A6:
len f <= i + (len f)
by NAT_1:11;
then
p .. f <= i + (len f)
by A4, XXREAL_0:2;
then A7:
(i + (len f)) -' (p .. f) < len f
by A5, NAT_D:54;
(len f) + 1 <= i + (len f)
by A2, XREAL_1:6;
then
((len f) + 1) -' (p .. f) <= (i + (len f)) -' (p .. f)
by NAT_D:42;
then
((len f) -' (p .. f)) + 1 <= (i + (len f)) -' (p .. f)
by A4, NAT_D:38;
then
((len f) - (p .. f)) + 1 <= (i + (len f)) -' (p .. f)
by A4, XREAL_1:233;
then A8:
len (f :- p) <= (i + (len f)) -' (p .. f)
by A1, FINSEQ_5:50;
(((i + (len f)) -' (p .. f)) + (p .. f)) -' (len f) =
(i + (len f)) -' (len f)
by A4, A6, XREAL_1:235, XXREAL_0:2
.=
i
by NAT_D:34
;
hence
LSeg (f,i) = LSeg ((Rotate (f,p)),((i + (len f)) -' (p .. f)))
by A1, A8, A7, Th31; verum