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)) /. 1 = p
let p be Element of D; :: thesis: for f being FinSequence of D st p in rng f holds
(Rotate (f,p)) /. 1 = p
let f be FinSequence of D; :: thesis: ( p in rng f implies (Rotate (f,p)) /. 1 = p )
assume p in rng f ; :: thesis: (Rotate (f,p)) /. 1 = p
then Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by Def2
.= (<*p*> ^ (f /^ (p .. f))) ^ ((f -: p) /^ 1) by FINSEQ_5:def 2
.= <*p*> ^ ((f /^ (p .. f)) ^ ((f -: p) /^ 1)) by FINSEQ_1:32 ;
hence (Rotate (f,p)) /. 1 = p by FINSEQ_5:15; :: thesis: verum