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