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 & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len 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 & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & len (f :- p) < i & i <= len f holds
(Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))

let f be FinSequence of D; :: thesis: ( p in rng f & len (f :- p) < i & i <= len f implies (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f)) )
assume that
A1: p in rng f and
A2: len (f :- p) < i and
A3: i <= len f ; :: thesis: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))
A4: len (f -: p) = p .. f by ;
A5: ( (i -' (len (f :- p))) + (len (f :- p)) = i & Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) ) by ;
not f -: p is empty by ;
then len (f -: p) >= 1 by NAT_1:14;
then A6: len ((f -: p) /^ 1) = (len (f -: p)) - 1 by RFINSEQ:def 1;
i + (p .. f) <= (p .. f) + (len f) by ;
then A7: (i + (p .. f)) -' (len f) <= p .. f by NAT_D:53;
A8: p .. f <= len f by ;
then (len f) - (p .. f) = (len f) -' (p .. f) by XREAL_1:233;
then A9: len (f :- p) = ((len f) -' (p .. f)) + 1 by ;
then A10: (len f) -' (p .. f) < i by ;
then A11: len f < i + (p .. f) by NAT_D:55;
then (len f) + 1 <= i + (p .. f) by NAT_1:13;
then 1 <= (i + (p .. f)) -' (len f) by NAT_D:55;
then A12: (i + (p .. f)) -' (len f) in Seg (p .. f) by A7;
i <= (p .. f) + ((len f) -' (p .. f)) by ;
then i -' ((len f) -' (p .. f)) <= p .. f by NAT_D:53;
then (i -' (((len f) -' (p .. f)) + 1)) + 1 <= p .. f by ;
then A13: i -' (len (f :- p)) <= (len (f -: p)) - 1 by ;
(((len f) -' (p .. f)) + 1) + 1 <= i by ;
then A14: 1 <= i -' (((len f) -' (p .. f)) + 1) by NAT_D:55;
then A15: i -' (((len f) -' (p .. f)) + 1) in dom ((f -: p) /^ 1) by ;
(len f) - (p .. f) = (len f) -' (p .. f) by ;
then 1 <= i -' (len (f :- p)) by ;
then i -' (len (f :- p)) in dom ((f -: p) /^ 1) by ;
hence (Rotate (f,p)) /. i = ((f -: p) /^ 1) /. (i -' (((len f) -' (p .. f)) + 1)) by
.= (f -: p) /. ((i -' (((len f) -' (p .. f)) + 1)) + 1) by
.= (f -: p) /. (i -' ((len f) -' (p .. f))) by
.= (f -: p) /. (i - ((len f) -' (p .. f))) by
.= (f -: p) /. (i - ((len f) - (p .. f))) by
.= (f -: p) /. ((i + (p .. f)) - (len f))
.= (f -: p) /. ((i + (p .. f)) -' (len f)) by
.= f /. ((i + (p .. f)) -' (len f)) by ;
:: thesis: verum