let x be set ; :: thesis: for f being FinSequence st f just_once_values x holds
(x .. f) + (x .. (Rev f)) = (len f) + 1

let f be FinSequence; :: thesis: ( f just_once_values x implies (x .. f) + (x .. (Rev f)) = (len f) + 1 )
assume A1: f just_once_values x ; :: thesis: (x .. f) + (x .. (Rev f)) = (len f) + 1
then A2: x in rng f by FINSEQ_4:5;
then A3: f = ((f -| x) ^ <*x*>) ^ (f |-- x) by FINSEQ_4:51;
then A4: len f = (len ((f -| x) ^ <*x*>)) + (len (f |-- x)) by FINSEQ_1:22
.= ((len (f -| x)) + ()) + (len (f |-- x)) by FINSEQ_1:22
.= ((len (f -| x)) + 1) + (len (f |-- x)) by FINSEQ_1:39 ;
not x in rng (f |-- x) by ;
then A5: not x in rng (Rev (f |-- x)) by FINSEQ_5:57;
Rev f = (Rev (f |-- x)) ^ (Rev ((f -| x) ^ <*x*>)) by
.= (Rev (f |-- x)) ^ (<*x*> ^ (Rev (f -| x))) by FINSEQ_5:63
.= ((Rev (f |-- x)) ^ <*x*>) ^ (Rev (f -| x)) by FINSEQ_1:32 ;
then A6: x .. (Rev f) = (len (Rev (f |-- x))) + 1 by ;
(len (f -| x)) + 1 = ((x .. f) - 1) + 1 by
.= x .. f ;
hence (x .. f) + (x .. (Rev f)) = (((len (f -| x)) + 1) + (len (Rev (f |-- x)))) + 1 by A6
.= (len f) + 1 by ;
:: thesis: verum