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;
thus Rev (f :- p) = Rev (<*p*> ^ (f |-- p)) by A2, Th41
.= (Rev (f |-- p)) ^ <*p*> by Th24
.= ((Rev f) -| p) ^ <*p*> by A1, Th86
.= (Rev f) -: p by A3, Th40 ; :: thesis: verum