let i be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f))
A4: (len f) -' (p .. f) <= (len f) -' i by ;
A5: p .. f <= len f by ;
then i <= len f by ;
then ((len f) -' (p .. f)) + i <= len f by ;
then A6: (i + (len f)) -' (p .. f) <= len f by ;
(len f) + 1 <= i + (len f) by ;
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 ;
then ((len f) - (p .. f)) + 1 <= (i + (len f)) -' (p .. f) by ;
then A7: len (f :- p) <= (i + (len f)) -' (p .. f) by ;
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
.= i by NAT_D:34 ;
hence f /. i = (Rotate (f,p)) /. ((i + (len f)) -' (p .. f)) by A1, A7, A6, Th17; :: thesis: verum