let D be non empty set ; :: thesis: for p being Element of D

for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

let f be FinSequence of D; :: thesis: ( p in rng f implies (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) )

A1: 1 <= len (f :- p) by Th6;

assume A2: p in rng f ; :: thesis: (Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

then p .. f <= len f by FINSEQ_4:21;

then reconsider x = (len f) - (p .. f) as Element of NAT by INT_1:5;

((len (f :- p)) -' 1) + (p .. f) = ((x + 1) -' 1) + (p .. f) by A2, FINSEQ_5:50

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

.= len f ;

hence (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) by A1, A2, Th9; :: thesis: verum

for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds

(Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

let f be FinSequence of D; :: thesis: ( p in rng f implies (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) )

A1: 1 <= len (f :- p) by Th6;

assume A2: p in rng f ; :: thesis: (Rotate (f,p)) /. (len (f :- p)) = f /. (len f)

then p .. f <= len f by FINSEQ_4:21;

then reconsider x = (len f) - (p .. f) as Element of NAT by INT_1:5;

((len (f :- p)) -' 1) + (p .. f) = ((x + 1) -' 1) + (p .. f) by A2, FINSEQ_5:50

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

.= len f ;

hence (Rotate (f,p)) /. (len (f :- p)) = f /. (len f) by A1, A2, Th9; :: thesis: verum