let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st f just_once_values p holds
Rev (f |-- p) = (Rev f) -| p
let p be Element of D; :: thesis: for f being FinSequence of D st f just_once_values p holds
Rev (f |-- p) = (Rev f) -| p
let f be FinSequence of D; :: thesis: ( f just_once_values p implies Rev (f |-- p) = (Rev f) -| p )
assume A1: f just_once_values p ; :: thesis: Rev (f |-- p) = (Rev f) -| p
then A2: p in rng f by FINSEQ_4:5;
then A3: p in rng (Rev f) by FINSEQ_5:57;
then reconsider n = (p .. (Rev f)) - 1 as Element of NAT by FINSEQ_4:21, INT_1:5;
(p .. f) + (p .. (Rev f)) = (len f) + 1 by A1, Th37;
then A4: n + (p .. f) = len f ;
Rev (f |-- p) = Rev (f /^ (p .. f)) by A2, FINSEQ_5:35
.= (Rev f) | n by A4, Th84
.= (Rev f) | (Seg n) ;
hence Rev (f |-- p) = (Rev f) -| p by A3, FINSEQ_4:def 5; :: thesis: verum