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