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
A3: p in rng f by A2, FINSEQ_4:60;
then A4: p in rng (Rev f) by FINSEQ_5:60;
A5: f /. 1 = f /. (len f) by A1, Def1;
reconsider j = (len (f :- p)) - 1 as Element of NAT by INT_1:18, NAT_1:14;
A6: j + 1 = len (f :- p) ;
A7: f -: p = <*((f -: p) /. 1)*> ^ ((f -: p) /^ 1) by A3, FINSEQ_5:32, FINSEQ_5:50
.= <*(f /. 1)*> ^ ((f -: p) /^ 1) by A3, FINSEQ_5:47 ;
A8: f :- p = ((f :- p) | j) ^ <*((f :- p) /. (len (f :- p)))*> by A6, FINSEQ_5:24
.= ((f :- p) | j) ^ <*(f /. (len f))*> by A3, FINSEQ_5:57 ;
thus Rev (Rotate f,p) = Rev ((f :- p) ^ ((f -: p) /^ 1)) by A3, Def2
.= (Rev ((f -: p) /^ 1)) ^ (Rev (f :- p)) by FINSEQ_5:67
.= (Rev ((f -: p) /^ 1)) ^ (<*(f /. (len f))*> ^ (Rev ((f :- p) | j))) by A8, FINSEQ_5:66
.= ((Rev ((f -: p) /^ 1)) ^ <*(f /. 1)*>) ^ (Rev ((f :- p) | j)) by A5, FINSEQ_1:45
.= (Rev (f -: p)) ^ (Rev ((f :- p) | j)) by A7, Th28
.= (Rev (f -: p)) ^ ((Rev (f :- p)) /^ 1) by A6, Th91
.= (Rev (f -: p)) ^ (((Rev f) -: p) /^ 1) by A2, Th93
.= ((Rev f) :- p) ^ (((Rev f) -: p) /^ 1) by A2, Th94
.= Rotate (Rev f),p by A4, Def2 ; :: thesis: verum