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:7;
then A3: p in rng (Rev f) by FINSEQ_5:60;
then p .. (Rev f) >= 1 by FINSEQ_4:31;
then reconsider n = (p .. (Rev f)) - 1 as Element of NAT by INT_1:18;
(p .. f) + (p .. (Rev f)) = (len f) + 1 by A1, Th41;
then A4: n + (p .. f) = len f ;
Rev (f |-- p) = Rev (f /^ (p .. f)) by A2, FINSEQ_5:38
.= (Rev f) | n by A4, Th90
.= (Rev f) | (Seg n) by FINSEQ_1:def 15 ;
hence Rev (f |-- p) = (Rev f) -| p by A3, FINSEQ_4:def 6; :: thesis: verum