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 <= len (f :- p) holds

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

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

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

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

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

assume that

A1: p in rng f and

A2: 1 <= i and

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

A4: i in dom (f :- p) by A2, A3, FINSEQ_3:25;

A5: i = (i -' 1) + 1 by A2, XREAL_1:235;

Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A1, Def2;

hence (Rotate (f,p)) /. i = (f :- p) /. i by A4, FINSEQ_4:68

.= f /. ((i -' 1) + (p .. f)) by A1, A5, A4, FINSEQ_5:52 ;

:: thesis: verum

for p being Element of D

for f being FinSequence of D st p in rng f & 1 <= i & i <= len (f :- p) holds

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

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

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

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

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

assume that

A1: p in rng f and

A2: 1 <= i and

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

A4: i in dom (f :- p) by A2, A3, FINSEQ_3:25;

A5: i = (i -' 1) + 1 by A2, XREAL_1:235;

Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A1, Def2;

hence (Rotate (f,p)) /. i = (f :- p) /. i by A4, FINSEQ_4:68

.= f /. ((i -' 1) + (p .. f)) by A1, A5, A4, FINSEQ_5:52 ;

:: thesis: verum