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 <*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 A1, FINSEQ_4:45;
then A5: not x in rng (Rev (f |-- x)) by FINSEQ_5:57;
Rev f = (Rev (f |-- x)) ^ (Rev ((f -| x) ^ <*x*>)) by A3, FINSEQ_5:64
.= (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 A5, Th36;
(len (f -| x)) + 1 = ((x .. f) - 1) + 1 by A2, FINSEQ_4:34
.= x .. f ;
hence (x .. f) + (x .. (Rev f)) = (((len (f -| x)) + 1) + (len (Rev (f |-- x)))) + 1 by A6
.= (len f) + 1 by A4, FINSEQ_5:def 3 ;
:: thesis: verum