let i be Nat; for D being non empty set
for p being Element of D
for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
let D be non empty set ; for p being Element of D
for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
let p be Element of D; for f being circular FinSequence of D st p in rng f & 1 <= i & i <= p .. f holds
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
let f be circular FinSequence of D; ( p in rng f & 1 <= i & i <= p .. f implies f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) )
assume that
A1:
p in rng f
and
A2:
1 <= i
and
A3:
i <= p .. f
; f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
A4:
(len f) -' (p .. f) <= (len f) -' i
by A3, NAT_D:41;
A5:
p .. f <= len f
by A1, FINSEQ_4:21;
then
i <= len f
by A3, XXREAL_0:2;
then
((len f) -' (p .. f)) + i <= len f
by A4, NAT_D:54;
then A6:
(i + (len f)) -' (p .. f) <= len f
by A5, NAT_D:38;
(len f) + 1 <= i + (len f)
by A2, XREAL_1:6;
then
((len f) + 1) - (p .. f) <= (i + (len f)) - (p .. f)
by XREAL_1:9;
then
((len f) - (p .. f)) + 1 <= i + ((len f) - (p .. f))
;
then
((len f) - (p .. f)) + 1 <= i + ((len f) -' (p .. f))
by A5, XREAL_1:233;
then
((len f) - (p .. f)) + 1 <= (i + (len f)) -' (p .. f)
by A5, NAT_D:38;
then A7:
len (f :- p) <= (i + (len f)) -' (p .. f)
by A1, FINSEQ_5:50;
len f <= i + (len f)
by NAT_1:11;
then (((i + (len f)) -' (p .. f)) + (p .. f)) -' (len f) =
(i + (len f)) -' (len f)
by A5, XREAL_1:235, XXREAL_0:2
.=
i
by NAT_D:34
;
hence
f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
by A1, A7, A6, Th17; verum