let i be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being 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 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 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 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 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, Th12; :: thesis: verum