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:7;
then not x in rng (f -| x) by FINSEQ_4:49;
then not x in rng (Rev (f -| x)) by FINSEQ_5:60;
then A3: not x in rng ((Rev f) |-- x) by A1, Th42;
x in rng (Rev f) by A2, FINSEQ_5:60;
hence Rev f just_once_values x by A3, FINSEQ_4:60; :: thesis: verum