let x be set ; :: thesis: for f being FinSequence st f just_once_values x holds
Rev f just_once_values x
let f be FinSequence; :: thesis: ( f just_once_values x implies Rev f just_once_values x )
assume A1: f just_once_values x ; :: thesis: Rev f just_once_values x
then A2: x in rng f by FINSEQ_4:5;
then not x in rng (f -| x) by FINSEQ_4:37;
then not x in rng (Rev (f -| x)) by FINSEQ_5:57;
then A3: not x in rng ((Rev f) |-- x) by A1, Th38;
x in rng (Rev f) by A2, FINSEQ_5:57;
hence Rev f just_once_values x by A3, FINSEQ_4:45; :: thesis: verum