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

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