let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st f is circular & f just_once_values p holds
Rev (Rotate (f,p)) = Rotate ((Rev f),p)

let p be Element of D; :: thesis: for f being FinSequence of D st f is circular & f just_once_values p holds
Rev (Rotate (f,p)) = Rotate ((Rev f),p)

let f be FinSequence of D; :: thesis: ( f is circular & f just_once_values p implies Rev (Rotate (f,p)) = Rotate ((Rev f),p) )
assume that
A1: f is circular and
A2: f just_once_values p ; :: thesis: Rev (Rotate (f,p)) = Rotate ((Rev f),p)
reconsider j = (len (f :- p)) - 1 as Element of NAT by ;
A3: f /. 1 = f /. (len f) by A1;
A4: p in rng f by ;
then A5: f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by
.= <*(f /. 1)*> ^ ((f -: p) /^ 1) by ;
A6: j + 1 = len (f :- p) ;
then A7: f :- p = ((f :- p) | j) ^ <*((f :- p) /. (len (f :- p)))*> by FINSEQ_5:21
.= ((f :- p) | j) ^ <*(f /. (len f))*> by ;
A8: p in rng (Rev f) by ;
thus Rev (Rotate (f,p)) = Rev ((f :- p) ^ ((f -: p) /^ 1)) by
.= (Rev ((f -: p) /^ 1)) ^ (Rev (f :- p)) by FINSEQ_5:64
.= (Rev ((f -: p) /^ 1)) ^ (<*(f /. (len f))*> ^ (Rev ((f :- p) | j))) by
.= ((Rev ((f -: p) /^ 1)) ^ <*(f /. 1)*>) ^ (Rev ((f :- p) | j)) by
.= (Rev (f -: p)) ^ (Rev ((f :- p) | j)) by
.= (Rev (f -: p)) ^ ((Rev (f :- p)) /^ 1) by
.= (Rev (f -: p)) ^ (((Rev f) -: p) /^ 1) by
.= ((Rev f) :- p) ^ (((Rev f) -: p) /^ 1) by
.= Rotate ((Rev f),p) by ; :: thesis: verum