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 & p .. f <= i & i <= len f holds

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

f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds

f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f <= i & i <= len f implies f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) )

assume that

A1: p in rng f and

A2: p .. f <= i and

A3: i <= len f ; :: thesis: f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

A4: 1 + (p .. f) <= i + 1 by A2, XREAL_1:6;

i + 1 <= (len f) + 1 by A3, XREAL_1:6;

then ( i <= i + 1 & (i + 1) - (p .. f) <= ((len f) + 1) - (p .. f) ) by NAT_1:11, XREAL_1:9;

then (i + 1) -' (p .. f) <= ((len f) - (p .. f)) + 1 by A2, XREAL_1:233, XXREAL_0:2;

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

(((i + 1) -' (p .. f)) -' 1) + (p .. f) = (((i -' (p .. f)) + 1) -' 1) + (p .. f) by A2, NAT_D:38

.= (i -' (p .. f)) + (p .. f) by NAT_D:34

.= i by A2, XREAL_1:235 ;

hence f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) by A1, A4, A5, Th9, NAT_D:55; :: thesis: verum

for p being Element of D

for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds

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

f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f & p .. f <= i & i <= len f holds

f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

let f be FinSequence of D; :: thesis: ( p in rng f & p .. f <= i & i <= len f implies f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) )

assume that

A1: p in rng f and

A2: p .. f <= i and

A3: i <= len f ; :: thesis: f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f))

A4: 1 + (p .. f) <= i + 1 by A2, XREAL_1:6;

i + 1 <= (len f) + 1 by A3, XREAL_1:6;

then ( i <= i + 1 & (i + 1) - (p .. f) <= ((len f) + 1) - (p .. f) ) by NAT_1:11, XREAL_1:9;

then (i + 1) -' (p .. f) <= ((len f) - (p .. f)) + 1 by A2, XREAL_1:233, XXREAL_0:2;

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

(((i + 1) -' (p .. f)) -' 1) + (p .. f) = (((i -' (p .. f)) + 1) -' 1) + (p .. f) by A2, NAT_D:38

.= (i -' (p .. f)) + (p .. f) by NAT_D:34

.= i by A2, XREAL_1:235 ;

hence f /. i = (Rotate (f,p)) /. ((i + 1) -' (p .. f)) by A1, A4, A5, Th9, NAT_D:55; :: thesis: verum