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 & 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 circular 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 circular 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 circular 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: p .. f <= len f by A1, FINSEQ_4:21;

then A5: (len f) - (p .. f) = (len f) -' (p .. f) by XREAL_1:233;

for p being Element of D

for f being circular 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 circular 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 circular 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 circular 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: p .. f <= len f by A1, FINSEQ_4:21;

then A5: (len f) - (p .. f) = (len f) -' (p .. f) by XREAL_1:233;

per cases
( i = len (f :- p) or i > len (f :- p) )
by A2, XXREAL_0:1;

end;

suppose A6:
i = len (f :- p)
; :: thesis: (Rotate (f,p)) /. i = f /. ((i + (p .. f)) -' (len f))

then A7:
i = ((len f) - (p .. f)) + 1
by A1, FINSEQ_5:50;

then i >= 1 by A5, NAT_1:11;

hence (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A1, A6, Th9

.= f /. (((len f) -' (p .. f)) + (p .. f)) by A5, A7, NAT_D:34

.= f /. (len f) by A4, XREAL_1:235

.= f /. 1 by Def1A

.= f /. (((len f) + 1) -' (len f)) by NAT_D:34

.= f /. ((i + (p .. f)) -' (len f)) by A7 ;

:: thesis: verum

end;then i >= 1 by A5, NAT_1:11;

hence (Rotate (f,p)) /. i = f /. ((i -' 1) + (p .. f)) by A1, A6, Th9

.= f /. (((len f) -' (p .. f)) + (p .. f)) by A5, A7, NAT_D:34

.= f /. (len f) by A4, XREAL_1:235

.= f /. 1 by Def1A

.= f /. (((len f) + 1) -' (len f)) by NAT_D:34

.= f /. ((i + (p .. f)) -' (len f)) by A7 ;

:: thesis: verum