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

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