let D be non empty set ; :: thesis: for f being FinSequence of D st f just_once_values f /. (len f) holds
(f /. (len f)) .. f = len f
let f be FinSequence of D; :: thesis: ( f just_once_values f /. (len f) implies (f /. (len f)) .. f = len f )
assume A1: f just_once_values f /. (len f) ; :: thesis: (f /. (len f)) .. f = len f
then reconsider f9 = f as non empty FinSequence of D by FINSEQ_4:5, RELAT_1:38;
((f /. (len f)) .. f) + 1 = ((f /. (len f)) .. f) + (((Rev f9) /. 1) .. (Rev f9)) by Th43
.= ((f /. (len f)) .. f) + ((f /. (len f)) .. (Rev f)) by FINSEQ_5:65
.= (len f) + 1 by A1, Th37 ;
hence (f /. (len f)) .. f = len f ; :: thesis: verum